That led the previous post which looked at posterior means for three Bayesian models, showing how the posterior mean is a weighted average of the prior mean and the mean of the new data. The weights are precisions, which means something different for each model.

For the beta-binomial model, variance may increase when seeing unexpected data (details here), but precision always increases.

For the normal-normal model precision is the reciprocal of variance. Every new data point makes precision go up and posterior variance go down.

The Poisson-gamma model may be the most interesting. As stated in the previous post, if data has a Poisson distribution with parameter λ, and λ has a gamma(α₀, β₀) prior distribution, then the posterior distribution on λ after observing k events over time t has a gamma(α₀ + k, β₀ + t) posterior distribution. Therefore the posterior variance is

(α₀ + k) / (β₀ + t)².

Note the posterior variance is an increasing function of k and a decreasing function of t. This means that the posterior variance increases every time an event is observed, and it decreases quadratically between observations.

Here’s an illustration. I simulated data from a Poisson process with λ and used a gamma(1, 1) prior on λ. Here’s a plot of the posterior variance.

How much should new data change your prior beliefs? When prior judgment and new information are in conflict, which one should be given the benefit of the doubt?

Bayesian data models provide a framework for making such decisions quantitative and objective. The choice of a data model is somewhat subjective—whether it’s a Bayesian model or not—but given a Bayesian model, the rules for updating the representation of your beliefs are objective. As some put it, you “turn the Bayesian crank.” A likelihood model and a prior on parameters together specify how new data changes the prior distribution into a posterior distribution.

We will make this more concrete with three examples.

Normal-normal model

Suppose that data X has a normal distribution with unknown mean μ and known variance σ², and we assume that a priori μ has a normal distribution with mean μ₀ and variance σ₀².

After observing x, the posterior distribution on μ also has a normal distribution, but with a different mean and variance. Its mean is somewhere between the prior mean and x. We will ignore the change in the variance for this post.

The posterior mean of μ is

This equation becomes more understandable when we introduce precisons τ = 1/σ² and τ₀ = 1/σ₀².

Then we have

which you can read as saying the posterior mean is the weighted average of the prior mean and x, with the weights given by the precision. Intuitively, you take the weighted mean of your conclusions from previous data and new data, weighting the mean according to how much confidence you have in each.

Beta-binomial model

Now let’s switch over to a different data model. Now assume X is a binary random variable, with probability of success p and probability of failure 1 − p, and we assume p has a beta(a, b) distribution.

After observing s successes and f failures, the posterior mean of the distribution on p becomes

We can rewrite this as

This says that the posterior mean is the weighted average of the prior mean a/(a + b) and the mean of the data s/n. The weights are the prior effective sample size a + b and the sample size of the new data n. In this example (effective) sample size is playing the role that precision played in the normal-normal model above.

Gamma-Poisson model

Suppose data have a Poisson distribution with parameter λ, and λ has a gamma(α₀, β₀) prior distribution [1]. And suppose you observe k events over time t. Then the posterior distribution of λ given the data has a gamma(α₀ + k, β₀ + t) prior distribution and the mean of the posterior distribution is given by

As before, the posterior mean is a weighted average of the prior mean and new data, and the weights are interpretable as some sort of measure of confidence, namely time. The variable t is directly time and the parameter β₀ is sort of an effective time, just as a + b is an effective sample size for the beta distribution.

Common thread

In each example the posterior mean is the weighted average of the prior mean and the mean of the data, with the weights given by a precision. However, precision means something different in each example. In the normal-normal model, precision is the reciprocal of variance, but in the beta-binomial model precision is sample size and in the Poisson-gamma model precision is time.

What all three examples have in common is that they are conjugate models using distributions from the “exponential family” of probability distributions. In technical terms, precision is the multiplicative factor on the sufficient statistic in the exponent of the posterior kernel.

Related posts

• Does additional data always reduce posterior variance?
• Diagram of probability distribution relationships
• Bayesian statistics consulting

[1] There are multiple conventions for parameterizing the gamma distribution. Here we’re using the shape-rate parameterization, where the mean is α/β.

Gilbreath’s conjecture is simple, but it’s also kinda weird. As I wrote before,

Paul Erdős speculated that Gilbreath’s conjecture is true but it would be 200 years before anyone could prove it. I find Erdős’s conjecture more interesting than Gilbreath’s conjecture.

The conjecture is hard in a way that, say, solving a nasty-looking differential equation is not. Over the last three centuries, mathematics has developed quite a toolbox for solving differential equations. But Gilbreath’s conjecture is just odd enough that it’s not at all clear what kind of tool might be useful in approaching it.

Terence Tao has a new blog post announcing a paper that he and two coauthors wrote on a random model intended to mimic Gilbreath’s calculation on primes. This random model is more sophisticated than the little game Gilbreath was playing, but it’s also much more amenable to analysis by established techniques. Tao’s post gives a heuristic explanation for why Gilbreath’s conjecture is plausible, but then adds

However, it seems well beyond current technology to try to make these heuristics rigorous; even the first step … is far out of reach.

Related posts

• Moessner’s Magic
• Closed form solutions to PDEs

The theorem corresponding to the diagram is interesting, but I found reproducing the diagram more interesting.

The segment AB is a diameter and the line CD is perpendicular to the diameter.

Assume the outer circle is a unit circle. I guessed C = (cos(1), sin(1)) and made the following diagram.

I guessed the value of C by eyeballing it, but in retrospect this would have been a convenient value for the creator of the original diagram to have chosen.

Drawing the blue circle inscribed in the triangle was easy using the equations for the center and radius from this post. Drawing the other two circles, the green and orange circles, was harder. They are also inscribed circles, but not inscribed in a triangle. They’re inscribed in a three-sided figure with two perpendicular sides and a circular arc.

The radius r of the green circle is the distance from the center of the circle to each of its tangent lines. Also, the distance from the origin to the center of the circle must be 1 − r. This is enough information to set up a quadratic equation for r. The same reasoning applies to the orange circle.

The original diagram comes from [1] and the theorem it illustrates says the diameter of the blue circle equals the sum of the radii of the green and orange circles.

Python code

In case you’re interested, here’s the code that created the diagram.

#!/usr/bin/env -S uv run --script

# /// script
# dependencies = ["numpy", "matplotlib"]
# ///

import numpy as np
import matplotlib.pyplot as plt

def connect(A, B, color='gray'):
    plt.plot([A[0], B[0]], [A[1], B[1]], color=color, linewidth=2)

def circle(c, r, color='gray'):
    t = np.linspace(0, 2*np.pi)
    plt.plot(c[0] + r*np.cos(t), c[1] + r*np.sin(t), color=color, linewidth=2)

def quadratic(a, b, c):
    det = b**2 - 4*a*c
    return ((-b - det**0.5)/(2*a), (-b + det**0.5)/(2*a))

A = np.array([-1, 0])
B = np.array([ 1, 0])
C = np.array([np.cos(1), np.sin(1)])
a = np.linalg.norm(B - C)
b = np.linalg.norm(A - C)
c = np.linalg.norm(B - A)
s = (a + b + c)/2

circle([0,0], 1)
connect(A, B,)
connect(A, C)
connect(C, B)
connect(C, C*np.array([1, -1]))

center = (a*A + b*B + c*C)/(2*s)
radius = 0.5*a*b/s
circle(center, radius, 'C0')

Ex = C[0]
roots = quadratic(1, 2 + 2*Ex, Ex**2 - 1)
r = roots[1] # Smaller root is negaive
print(roots)
center = (r + Ex, -r)
circle(center, r, 'C1')

roots = quadratic(1, 2 - 2*Ex, Ex**2 - 1)
r = roots[1] # Smaller root is negaive
center = (Ex - r, -r)
circle(center, r, 'C2')

plt.gca().set_aspect("equal")
plt.axis("off")
plt.show()

[1] Leon Bankoff. A Geometrical Coincidence. Mathematics Magazine, Vol. 37, No. 5 (Nov., 1964), p. 324.

e ≈ 2721/1001

recently. What makes this remarkable is its accuracy relative to the size of the denominator.

You can create a trivial approximation just by truncating a decimal expansion

e ≈ 2718/1000

but this is only good to four significant figures, but 2721/1001 is good to seven, almost eight, significant figures.

e         = 2.71828182… 
2721/1001 = 2.71828171…

The comparison is more impressive in binary.

$ bc -l
>>> obase=2
>>> 2721/1001
10.10110111111000010100…
>>> e(1)
10.10110111111000010101…

The denominator is a 10-bit number but the approximation is accurate to 21 bits.

In general, new information reduces your uncertainty regarding whatever you’re estimating. The posterior distribution becomes more concentrated as more data are collected.

That’s what happens “in general” but does it necessarily happen every time you get new data? Conceivably if you get surprising data, data that is very unlikely given your current prior, posterior uncertainty might increase.

Beta-binomial model

To show that this is the case, suppose the probability of success in some binary trial has parameter θ and that θ has a beta prior. You could imagine this prior to be the posterior after having made some number of previous observations. Can a new observation increase the posterior variance in θ? If so, under what conditions?

The variance of a beta(a, b) random variable is

ab / (a + b)²(a + b + 1).

After observing a successful trial, the posterior distribution on θ is beta(a + 1, b). We can calculate the ratio of the posterior variance to the prior variance and ask under what circumstances, if any, the ratio is greater than 1.

If 2a ≥ b the posterior variance will be strictly less than the prior variance. This says if the prior mean odds against a success are no more than 2 : 1, observing a success will reduce the variance. (So will observing a failure.) But for any value of b, you can find a small enough value of a that observing a success will increase the variance.

Normal-normal model

Whether an observation can increase the posterior variance depends on the data model. If your data have a normal likelihood function with known variance and a normal prior on the mean θ, the posterior variance is always less than the prior observation, and it reduces by the same amount, independent of the observation x. If x is very unlikely a priori then it will pull the posterior mean toward itself more than an observation that is more concordant with the prior would have, but the change in the posterior variance is the same.

Proof of beta theorem

Here is a proof in Lean 4 of the statement above that if 2a ≥ b the posterior variance will be strictly less than the prior variance.

import Mathlib

set_option linter.style.header false

noncomputable def f (a b : ℝ) : ℝ := a * b / ((a + b) ^ 2 * (a + b + 1))

theorem f_ratio_lt_one' (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : b ≤ 2 * a) :
    f (a + 1) b / f a b < 1 := by
  have hs : 0 < a + b := by linarith
  have h2ab : 0 ≤ 2 * a - b := by linarith
  have hprod : 0 ≤ (a + b) * (2 * a - b) := mul_nonneg hs.le h2ab
  -- key polynomial inequality (∗)
  have key : (a + 1) * (a + b) ^ 2 < a * ((a + b + 1) * (a + b + 2)) := by
    nlinarith [hprod, ha]
  -- nonzero facts needed to clear denominators
  have ha' : a ≠ 0 := ne_of_gt ha
  have hb' : b ≠ 0 := ne_of_gt hb
  have hs' : a + b ≠ 0 := ne_of_gt hs
  have hs1' : a + b + 1 ≠ 0 := by positivity
  have hs2' : a + b + 2 ≠ 0 := by positivity
  have ha1' : a + 1 ≠ 0 := by positivity
  -- express the ratio as a single closed-form fraction
  have hratio : f (a + 1) b / f a b
      = ((a + 1) * (a + b) ^ 2) / (a * ((a + b + 1) * (a + b + 2))) := by
    unfold f
    have e : a + 1 + b = a + b + 1 := by ring
    rw [e]
    field_simp
    ring
  rw [hratio, div_lt_one (by positivity)]
  exact key

The more general Delannoy numbers D_m,n are the analogy for an m × n rectangular board, not necessarily square.

D_m,n is also the number of possible sequence alignments for a strand of DNA with m base pairs and a strand with n base pairs [1]. At each step in the alignment process, you can introduce a gap in the first strand, the second strand or neither, which is analogous to the king who can move N, E, or NE at each step.

The Delannoy numbers can be computed recursively:

def D(m, n):
    if m == 0 or n == 0:
        return 1
    return D(m - 1, n) + D(m, n - 1) + D(m - 1, n - 1)

The code above can be sped up tremendously by adding the decorator

@lru_cache(maxsize=None)

above the function definition to turn on memoization. I did an experiment computing D_12,15 with and without memoization and the times were 77.1805 seconds and 0.000062 seconds respectively, i.e. memoization made the code over a million times faster.

Incidentally, D_12,15 = 2653649025 and so there are a lot of ways to align even short sequences unless you place some restriction on the permissible alignments.

Update: Here’s a heatmap plotting log₁₀(D_m,n). Obviously the function increases with m and n: bigger chessboards have more possible paths. Moreover, it’s larger along the diagonal (i.e. the central Delannoy numbers). If you look along northeast to southwest diagonals, the function is largest in the middle where m = n.

[1] Torres, A., Cabada, A., & Nieto, J. J. (2003). An exact formula for the number of alignments between two DNA sequences. DNA Sequence, 14(6), 427–430. https://doi.org/10.1080/10425170310001617894

Professor: f is a function of a real variable x that takes a real parameter k.

Student: What’s a parameter?

Professor: It’s a constant that can vary.

Student: Then if it can vary, isn’t it a variable?

Professor: Sorta, but no not really.

This conversation plays out over and over, and unfortunately it often ends as it does above, with the student confused. Here’s how I believe the conversation should continue.

Professor: You’re absolutely right that f is a function of two variables, x and k. But usually k is fixed in the context of a specific application and x is not. A different application might have a different, but also fixed, value of k. So it is helpful to think of f(x; k), a function of x with a parameter k, rather than f(x, k), a function of two variables. The former carries more information, giving a hint as to how the numbers are used.

Is there really a difference between a parameter and a variable? In a reductionistic sense, no. But in a practical sense, yes, absolutely.

It might sound pedantic to distinguish a variable from a parameter, and it is, in the best sense of the word. Pedant literally means teacher. Usually pedantic carries a negative connotation, such as making a distinction without a difference. But here the pedant would be making a helpful distinction.

For example, we might write a probability density function as f(x; μ, σ). The function gives the probability density at a point x. The density depends on parameters μ and σ, and these parameters change between applications, but for a given application they have fixed values.

You find the probability of a random variable taking on values in an interval [a, b] by integrating f over that interval. When I say that, you know that I mean you’d integrate with respect to x, because f is a function of x. It is also, in an abstract sense, a function of μ and σ, but it’s typically not useful to think of it that way.

Hypergeometric functions have two sets of parameters, and so you may see two semicolons, such as f(x; a, b; c). This denotes a function of the variable x, with upper parameters a and b, and a lower parameter c. In some abstract sense this is a function of four variables, but it acts very differently with respect to x than with respect to a, b, and c. There’s also a difference between a and b on the one hand and c on the other, one worth paying attention to, though it is less of a difference than between x and the parameters collectively.

Sometimes you’ll see a vertical bar rather than a semicolon to separate variables from parameters. This works out even better for probability densities because then f(x | μ, σ) suggests the probability density of x given μ and σ since the vertical bar is also used for conditional probability. You might also see f(x | a, b; c) for hypergeometric functions, with the vertical bar separating variables from parameters and the semicolon separating two kinds of parameters.

When I first saw a semicolon separating variables from parameters, no explanation was given, and I figured I could mentally replace the semicolon with a comma. Then later I realized that the semicolon was an act of kindness by the author giving the reader additional information.

The defining property of golden rectangle is that if you stick a square on its longer side, you get another golden rectangle.

The smaller vertical rectangle is similar to the larger horizontal rectangle. This means

φ / 1 = (1 + φ) / φ

which tells us φ² = 1 + φ and so the golden ratio φ equals (1 + √5)/2.

Silver rectangles

A silver rectangle is one that if you stick two squares on its longer side you get another rectangle with the same aspect ratio.

This tells us

σ / 1 = (1 + 2σ) / σ

and so σ² = 1 + 2σ and the silver ratio is σ = 1 + √2.

Just as you can define a golden ratio and a silver ratio, there’s an analogous way to define a sequence of metallic ratios.

Kings and Delannoy numbers

The silver ratio has several connections to the ways of ways kings. By that I mean the number of ways a king can go from one corner of a chessboard to the diagonally opposite corner without backtracking.

A king can move one space in any direction. If we start with a king in the bottom left corner of the board, the no-backtracking requirement means the king can move up, right, or up and right.

The number of paths a king can take from one corner to the opposite corner of an n × n chessboard is the nth central Delannoy number D_n. more generally Delannoy numbers are defined for an m × n chessboard, but I’ll stick to the case m = n called the central Delannoy number, or just Delannoy numbers for short.

The first Delannoy number is 1 because there’s only one way for a king to get from one corner to the other: do nothing, because the opposite corner is the same corner. The second Delannoy number is 3 because the king can move up then right, or right then up, or move diagonally up and right.

For a 3 × 3 grid things are significantly more complicated, and D₃ = 13. For an 8 × 8 grid the number of paths is 48,639.

Generating function

How would you estimate the number of paths on an n × n board for large values of n without calculating it exactly? You might start by finding a generating function for the Delannoy numbers, which works out to be

(x² − 6x + 1)^−1/2

The radius of convergence r for the generating function series is the distance from 0 to the closest singularity of the generating function, which is the smaller root of

x² − 6x + 1

which is

3 − √8 = (3 + √8)⁻¹ = (1 + √2)⁻² = 1/σ²

i.e. the radius of convergence is the reciprocal of the silver ratio squared.

Asymptotic estimate

The radius of convergence gives us a first approximation to the asymptotic size of the series coefficients. Since we’re working with the generating function of the Delannoy numbers, these coefficients are the Delannoy numbers. That is,

D_n ~ r⁻ⁿ = (σ²)ⁿ = σ²ⁿ.

That’s as good as you can do just knowing the radius of convergence. A more careful analysis would refine this estimate by dividing by a factor proportional to √n.

Related posts

• The silver ratio
• A magic king’s tour

f ′(x) = f⁻¹(x)

This is a differential equation, but a very unusual one, one that cannot be solved using any of the techniques taught in a class on differential equations.

The unique solution is

f(x) = φ(x / φ)^φ

where φ is the golden ratio. What an unexpected appearance of the golden ratio!

The problem was proposed by H. L. Nelson and solved by A. C. Hindmarsh. See The American Mathematical Monthly, Vol. 76, No. 6 p. 696.

The bc function j takes two arguments. Is the first argument n or x? Grok said the function arguments are j(n,x). I thought I should run man bc just to make sure, and it said

j(x, n) Returns the bessel integer order n (truncated) of x.

So Grok says j(n,x) and the documentation that ships with the software says j(x,n). Which one should you believe? Neither! You should run a little test.

~$ bc -l
>>> j(1, 0)
0
>>> j(0, 1)
.76519768655796655144

Now J₁(0) = 0, so apparently the first argument is the order n. Grok was right and the man page was wrong.

As further confirmation, let’s see which argument is truncated.

>>> j(1.2, 3.4)
.17922585168150711099
>>> j(1, 3.4)
.17922585168150711099
>>> j(1.2, 3)
.33905895852593645892

The first argument is truncated to an integer value, so that’s the order n.

Turns out there’s a bug in the man page. The man page text above comes from running man bc on my Macbook. On my Linux box, the documentation is correct. It says

j(n,x) The Bessel function of integer order n of x.

The software produces the same results on both computers. It’s just a documentation bug.

The version running on my Macbook is the version that ships with the OS. It’s not the Gnu version, though the documentation says “This bc is compatible with both the GNU bc and the POSIX bc spec.” It has a function t for tangent, for example, which a POSIX version does not. But if you run bc --standard -l attempting to call t produces an error.

echo {w,t,}h{e{n{,ce{,forth}},re{,in,fore,with{,al}}},ither,at}

This prints 30 English words:

when, whence, whenceforth, where, wherein, wherefore, wherewith, wherewithal, whither, what, then, thence, thenceforth, there, therein, therefore, therewith, therewithal, thither, that, hen, hence, henceforth, here, herein, herefore, herewith, herewithal, hither, hat

This post will explain how the one-liner works.

Bash brace expansion iterates through all possibilities listed within curly braces, with possibilities separated by a comma. Note that the comma is a separator and not a terminator. And so, for example, the expression {w,t,} is effectively {w,t,""}.

When bash sees two brace expressions, these expand to the cartesian product of the two expressions. For example,

echo {A,B}{1,2,3}

produces

A1 A2 A3 B1 B2 B3

In the expression above we have

{w,t,}h{e…,ither,at}

So the expansion will enumerate all possibilities of {w,h,} multiplied by all possibilities of {e…,ither,at} where e… is itself a brace expression.

A diagram will help a lot.

The brace expansion does a depth-first traversal of this tree.

I wrote about the period length for the digits of fractions almost a decade ago. This post includes code so I can apply it to harmonic denominators.

from sympy import lcm, factorint, n_order

def period(n):
    factors = factorint(n)
    exp2 = factors.get(2, 0)
    exp5 = factors.get(5, 0)
    r = max(exp2, exp5)

    d = n // (2**exp2 * 5**exp5)
    s = 1 if d == 1 else n_order(10, d)
    return (r, s)

This function returns two numbers: r is the number of non-repeating digits at the beginning and s is the length of the repeating part.

The following code

from functools import reduce

def lcm_range(n):
    return reduce(lcm, range(1, n + 1))

print( period( lcm_range(50) ) )

prints (5, 1275120) meaning that 1/lcm(1, 2, 3, …, 49, 50) has five non-repeating digits following by 1,275,120 digits that repeat ad infinitum. And so the decimals in the expansion of H₅₀ have a cycle length of 1,275,120.

We’ll choose our base b to be 2. And we’ll look at the total number of bits in both the numerator and denominator, which we will use as the height of the fractions.

First, let’s look at the actual and estimated heights, using the estimates from the previous post.

Next let’s look at the difference between the actual and estimated heights.

In the previous post I looked at n = 50, which was kind of a lucky choice, the error being smaller than usual. I had also looked at, but didn’t publish, n = 100, which would be an unlucky choice.

Finally, let’s look at the relative error in the estimates, and plot over a larger range of n.

The error goes to zero, as predicted by the asymptotic estimates. And it goes noisily, which you’d expect since the heights are related to the distribution of primes.

H_n = 1 + 1/2 + 1/3 + 1/4 + … + 1/n

The product of all the denominators is n!, so you could write H_n as a fraction

H_n = p/q

where p = n! H_n is an integer and q = n!.

While p/q is a way to write H_n as a fraction, it’s not the most efficient because p and n! will have common factors.

If we write H_n as a reduced fraction, the denominator will be the least common multiple of the integers 1 through n. That number is asymptotically exp(n). That estimate follows from the prime number theorem.

So for large n the denominator will be roughly exp(n), and in base b it would have around

n/log(b)

digits.

The numerator will be exp(n) H_n, and since H_n is asymptotically log(n) + γ, the numerator for large n will be roughly

exp(n) (log(n) + γ)

and will have around

(n + log log(n) ) / log(b)

digits.

Let’s see how well our asymptotic estimates work for n = 50. The 50th harmonic number is

H₅₀ = 13943237577224054960759 / 3099044504245996706400.

This fraction has 23 digits in the numerator and 22 in the denominator. We would have predicted around

(50 + log(log(50)))/log(10) = 22.3

digits in the numerator and

50/log(10) = 21.7

digits in the denominator.

Let’s try a larger example, looking at the 1000th harmonic number in binary. We’ll use the following Python code.

from fractions import Fraction

def bits(n):
    H = sum(Fraction(i, i+1) for i in range(1, n+1))
    p, q = H.numerator, H.denominator
    # subtract 2 because bin returns a string starting with 0b.
    return len(bin(p)) - 2, len(bin(q)) - 2

print(bits(1000))

This returns 1448 and 1438. We would have estimated

(1000 + log(log(1000)))/log(2) = 1445.4

bits in the numerator and

1000/log(2) = 1442.7

bits in the denominator.

Update: See the next post for plots as a function of n.

Related posts

• Computing harmonic numbers
• Sums of consecutive reciprocals
• AM over GM

If a triangle be formed by the arcs of three circles, the inscribed and the three escribed circles are all tangent to a new circle or line.

Here “triangle” means a three-sided figure whose sides are portions of a circle. The inscribed circle is the largest circle that can fit inside the three-sided figure.

The “escribed” circles are analogous to the excircles in the previous post: you extend two sides and find a circle that is tangent to the triangle side and the extended side. The difference here being that the side extensions are now circles.

In the process of writing the latter, I looked at the Wikipedia article on Pythagorean triples and noticed this curious paragraph.

In every Pythagorean triangle, the radius of the incircle and the radii of the three excircles are positive integers. Specifically, for a primitive triple the radius of the incircle is r = n(m − n), and the radii of the excircles opposite the sides m² − n², 2mn, and the hypotenuse m² + n² are respectively m(m − n), n(m + n), and m(m + n).

The citation for the paragraph above was the book by my former officemate, which led to the post on the Star Trek lemma. The passage in Arthur Baragar’s book that Wikipedia cites is Exercise 15.3.

Let ΔABC be a right angle triangle with sides of integer length. Prove that the inradius r and the exradii r_a, r_b, and r_c are all integers.

I don’t know whether Arthur discovered this theorem, but I’ll call it Baragar’s theorem for this post.

Incircles and excircles

To unpack Baragar’s theorem, let’s start by saying what incircles and excircles are. Incircles are more familiar. The incircle of a triangle is the largest circle that can be inscribed inside the triangle, and the radius of this circle is the inradius.

Since an incircle is an inscribed circle, you might expect an excircle to be a circumscribed circle, but that’s not it. There are three excircles, one for each side. To find the excircle for a side, extend the other two sides and find the circle tangent to the side and the two extensions. The radius of an excircle is its exradius.

Proof

Baragar’s theorem follows directly from Euclid’s formula for Pythagorean triples mentioned in the previous post

and formulas for the inradius r and the exradii r_a, r_b, and r_c.

Here K is the area of the triangle, which in our case is ab/2, and s is the semiperimeter, half the perimeter.

Expressing the radii in terms of m and n gives the values cited by Wikipedia above.

Illustrating the theorem

I’d like to write a Python script to illustrate the theorem, and knowing the radii of the circles help, but we also need to know the centers of the circles.

The center of the incircle is the weighted average of the vertices, with weights given by the lengths of the opposite sides. That is, if the vertices are A, B, and C, and the sides opposite these vertices are a, b, and c, the the incenter is

The centers for the excircles have remarkably similar expressions. For the incenter of the circle opposite a vertex, flip the sign of the corresponding side.

Python code

Putting it all together, here’s an illustrate the theorem.

And here’s the code that produced it. Note that everything in this section works for right triangles in general, not just Pythagorean triangles.

import numpy as np
import matplotlib.pyplot as plt

def connect(A, B):
    plt.plot([A[0], B[0]], [A[1], B[1]], "C0")

def draw_circle(c, r, color):
    t = np.linspace(0, 2*np.pi)
    plt.plot(r*np.cos(t) + c[0], r*np.sin(t) + c[1], color=color)

a, b, c, = 3, 4, 5

A = np.array([0, b])
B = np.array([-a, 0])
C = np.array([0, 0])

s = (a + b + c)/2
K = a*b/2
r = K/s
ra = K/(s - a)
rb = K/(s - b)
rc = K/(s - c)
I = (a*A + b*B + c*C)/(a + b + c)
Ia = (-a*A + b*B + c*C)/(-a + b + c)
Ib = (a*A - b*B + c*C)/(a - b + c)
Ic = (a*A + b*B - c*C)/(a + b - c)

draw_circle(I, r, "C1")
draw_circle(Ia, ra, "C2")
draw_circle(Ib, rb, "C3")
draw_circle(Ic, rc, "C4")

plt.plot([-2*rc, 2*rb], [0, 0], "C0")
plt.plot([0, 0], [-2*ra, 2*rc], "C0")
plt.plot([(-2*ra - b)*a/b, 2*rb], [-2*ra, 2*rb*b/a + b], "C0")

plt.gca().set_aspect("equal")
plt.show()

a + 1 = b

George Osborne wrote a paper [1] addressing the question of when the squares of two consecutive numbers is also a square. Geometrically this is asking for primitive Pythagorean triples for which the legs are consecutive integers.

He proved that the sequence shorter legs satisfies the recurrence relation

with initial conditions u₀ = 0 and u₁ = 1. This is OEIS sequence A001652.

The method for solving recurrences like the one above is analogous to the method for solving linear differential equations. See a solution here. This gives us the following formula for the terms:

b + 1 = c

It’s also possible for the longer side and hypotenuse of a Pythagorean triangle to be consecutive numbers, as in the (5, 12, 13) triangle.

All primitive Pythagorean triples are given by Euclid’s formula

with integers m > n > 0. If b and c are consecutive numbers, then

and so m = n + 1. Therefore all possible values of b are given by 2n(n + 1) for n > 1.

[1] Geo. A. Osborne. A Problem in Number Theory. The American Mathematical Monthly, Vol. 21, No. 5 (May, 1914), pp. 148-150

I found his book on Archive.org and was surprised to see “The Star Trek Lemma” in the table of contents. What could this be?

It’s a theorem that goes back to Euclid that applies to an angle formed by connecting a point to two other points on a circle. The theorem says “The measure of an inscribed angle is half the measure of the arc it subtends.” But why call it the Star Trek lemma? Quoting Arthur:

In the spirit of Euclid, we will refer to this theorem as the Star Trek lemma because of the figure associated with the statement of the theorem. … Before Star Trek, as far as I know, this theorem had no name, though some might call it Euclid III.20, which is its proposition number in Euclid’s Elements (Book III, Proposition 20).

Here is my reconstruction of the figure given in the book.

The lemma says that ∠BAC is half of ∠BOC.

[1] Baragar, Arthur (2001), A Survey of Classical and Modern Geometries: With Computer Activities, Prentice Hall

I learned regular expressions in the context Perl, a maximalist regex environment. This led to frustration when features I expect to work are missing [1]. One way around this is to use Perl analogs of other tools, but this is very non-standard. I want to be able to send colleagues and clients code that works out of the box.

As I mentioned in my post on computational survivalism, I occasionally need to work on computers that I cannot install software on. So a better approach is to identify a subset of regex features that work everywhere. The stricter your definition of “everywhere” the less this includes. The strictest subset would be

• literals
• character classes […]
• the special characters . * ^ $

A more relaxed definition of “everywhere” would be the tools you most care about. Currently the tools I most want to use with regular expressions are sed, awk, grep, and Emacs.

Awk as lowest common denominator

If you use the Gnu versions of sed, awk, and grep, and use the -E option with sed and grep, then the list of common features is bigger. The regular expression features of the three tools are similar, and awk’s features are supported in the other tools, with one exception: word boundaries in awk are \< and \> rather than \b and \B.

I wrote about Awk’s regex features here.

Emacs as the oddball

Emacs supports analogs of most of awk’s regex features. However, the characters

    + ? ( ) { } |

all require a backslash in front in order to act like the awk counterparts. Also, the analog of \s and \S in awk is \s- and \S- in Emacs.

Instead of meaning space or nonspace, \s and \S in Emacs begin a (negated) character class, and one of those classes is - for space. But there are many others. For example, \s. stands for a punctuation character and \S. stands for a non-punctuation character.

What works everywhere

So for my definition of “everywhere,” with the caveats mentioned above, the following features work everywhere. YMMV.

    .
    ^, $
    […], [^…]
    *
    \w, \W, \s, \S
    \1 - \9 backreferences
    \b \B
    ? + 
    | alternation
    {n,m} for counting matches
    (...) capturing

One footnote is that gawk supports backreferences in replacement strings but not in regular expressions per se.

[1] To some extent, basic Perl features work elsewhere and advanced features do not, depending on your idea of what is basic or advanced. I think of look-around features as advanced, and that tracks. But I think of \d for digits as basic, but that’s not supported in many regex flavors.

This theorem is useful in Fourier analysis and signal processing. It’s useful to know even in the special case f(x) = 1.

For a “jinc” analog, see this paper.

***

Every time I see the name Lobachevsky I think of Tom Lehrer’s song about him. You can find the words here and the audio here.

Related posts

• Sinc and jinc integrals
• Sinc and jinc sums

When n is a prime number ≥ 5, it is sufficient to place the queens on a line that has slope 2, 3, 4, …, n − 2. (The slope cannot be 1 because that’s a diagonal. And it cannot be n − 1 because n − 1 = −1 mod n is also a diagonal.) [1]

Here we imagine opposite edges of the board being joined together. Geometrically, this makes the chessboard a torus (donut). Algebraically, the points on a line of slope s have the coordinates

(a + k, b + ks)

where addition is carried out mod n.

All solutions to the n queens problem have this form when n = 5. Some solutions will have this form for larger prime values of n but not all.

For example, when n = 7, here is a solution where all the queens are on a line of slope 2.

But here is another solution where the queens do not all lie on a line of constant slope.

Related posts

• Formulating eight queens as a SAT problem
• Queens on a donut
• Solving a chess puzzle with Claude and Prolog

[1] W. H. Bussey. A Note on the Problem of the Eight Queens. The American Mathematical Monthly, Vol. 29, No. 7 (August 1922), pp. 252–253

The puzzle is one I’ve written about before:

Place all the pieces—king, queen, two bishops, two knights, and two rooks—on a 6 × 5 chessboard, with the requirement that the two bishops be on opposite colored squares and no piece is attacking another.

Incidentally, it’s common for “piece” to exclude pawns, as above. But then what do you call all the things on a chessboard? You might call them “chess pieces,” in which case a pawn is a “chess piece” but not a “piece.” One convention is to use “chessmen” or simply “men” to include pieces and pawns.

This was the prompt I used.

Write Z3/Python code to find all solutions to the following chess puzzle.

Place all the pieces—king, queen, two bishops, two knights, and two rooks—on a 6 × 5 chessboard, with the requirement that the two bishops be on opposite colored squares and no piece is attacking another.

The code found 192 = 8 × 24 solutions. The factor of 8 comes from 2³ ways of swapping the pairs of bishops, knights, and rooks. The script reports

Total raw solutions: 192
Unique solutions (deduplicating piece-pair swaps): 24

── Solution 1 ──
  0 1 2 3 4
0 . K . . N
1 . . . . B
2 . . R . .
3 Q . . . .
4 . . . R .
5 . B . . N
  King: (0,1)
  Queen: (3,0)
  Bishop1: (5,1) [light]
  Bishop2: (1,4) [dark]
  Knight1: (5,4)
  Knight2: (0,4)
  Rook1: (4,3)
  Rook2: (2,2)

── Solution 2 ──
  0 1 2 3 4
0 N . . K .
1 B . . . .
2 . . R . .
3 . . . . Q
4 . R . . .
5 N . . B .
  King: (0,3)
  Queen: (3,4)
  Bishop1: (5,3) [light]
  Bishop2: (1,0) [dark]
  Knight1: (5,0)
  Knight2: (0,0)
  Rook1: (4,1)
  Rook2: (2,2)

...

── Solution 24 ──
  0 1 2 3 4
0 B . . B .
1 N . . . .
2 . . . . Q
3 . . R . .
4 . R . . .
5 N . . K .
  King: (5,3)
  Queen: (2,4)
  Bishop1: (0,0) [light]
  Bishop2: (0,3) [dark]
  Knight1: (5,0)
  Knight2: (1,0)
  Rook1: (3,2)
  Rook2: (4,1)

Here’s the code.

"""
Chess Puzzle Solver using Z3
Place king, queen, 2 bishops, 2 knights, 2 rooks on a 6×5 board
such that:
  - The two bishops are on opposite-colored squares
  - No piece attacks any other piece
"""

from z3 import (
    Int, Solver, Or, And, Not, Distinct, If,
    sat, ForAll, Implies
)
import itertools

ROWS = 6
COLS = 5
TOTAL_CELLS = ROWS * COLS  # 30

PIECES = ["king", "queen", "bishop1", "bishop2", "knight1", "knight2", "rook1", "rook2"]
N = len(PIECES)  # 8 pieces

def cell(r, c):
    return r * COLS + c

def pos_to_rc(pos):
    return pos // COLS, pos % COLS

def color(r, c):
    """Square color: 0=light, 1=dark"""
    return (r + c) % 2

def attacks_king(r1, c1, r2, c2):
    return max(abs(r1 - r2), abs(c1 - c2)) == 1

def attacks_queen(r1, c1, r2, c2):
    return (r1 == r2 or c1 == c2 or
            abs(r1 - r2) == abs(c1 - c2))

def attacks_bishop(r1, c1, r2, c2):
    return abs(r1 - r2) == abs(c1 - c2)

def attacks_rook(r1, c1, r2, c2):
    return r1 == r2 or c1 == c2

def attacks_knight(r1, c1, r2, c2):
    dr, dc = abs(r1 - r2), abs(c1 - c2)
    return (dr == 1 and dc == 2) or (dr == 2 and dc == 1)

# Map piece index to its attack function
ATTACK_FN = {
    0: attacks_king,
    1: attacks_queen,
    2: attacks_bishop,
    3: attacks_bishop,
    4: attacks_knight,
    5: attacks_knight,
    6: attacks_rook,
    7: attacks_rook,
}

def solve_all():
    solutions = []

    # Each piece gets an integer position in [0, TOTAL_CELLS)
    pos = [Int(f"pos_{p}") for p in PIECES]

    s = Solver()

    # All positions in valid range
    for p in pos:
        s.add(p >= 0, p < TOTAL_CELLS)

    # All pieces on distinct squares
    s.add(Distinct(*pos))

    # Bishops on opposite colors
    # bishop1 = pos[2], bishop2 = pos[3]
    # color of pos = ((pos // COLS) + (pos % COLS)) % 2
    b1_color = (pos[2] / COLS + pos[2] % COLS) % 2  # Z3 integer arithmetic
    b2_color = (pos[3] / COLS + pos[3] % COLS) % 2

    # Z3 doesn't do Python //; use integer division carefully
    # We'll encode opposite colors: sum of colors == 1
    # color(pos) = (row + col) % 2 = (pos//COLS + pos%COLS) % 2
    # For Z3 int vars, use: (pos / COLS + pos % COLS) % 2
    s.add((pos[2] / COLS + pos[2] % COLS) % 2 != (pos[3] / COLS + pos[3] % COLS) % 2)

    # No piece attacks another
    # We enumerate all (i,j) pairs and for each possible (pos_i, pos_j) assignment,
    # assert that those pieces don't attack each other.
    # Since positions are Z3 vars, we use a constraint table approach:
    # For each pair (i,j), add constraints over all concrete (r1,c1,r2,c2) combos.

    # Pre-build attack lookup tables for each piece-type pair
    # This avoids slow Z3 symbolic reasoning over large disjunctions.

    # We'll encode: for all concrete assignments, if pos[i]==cell(r1,c1) and pos[j]==cell(r2,c2),
    # then piece i must not attack piece j.
    # Equivalently: NOT (pos[i]==cell(r1,c1) AND pos[j]==cell(r2,c2)) for all attacking pairs.

    # For efficiency, we build a set of "forbidden (cell_i, cell_j)" pairs per piece pair.

    for i, j in itertools.combinations(range(N), 2):
        fn_i = ATTACK_FN[i]
        fn_j = ATTACK_FN[j]
        forbidden = []
        for r1, c1 in itertools.product(range(ROWS), range(COLS)):
            for r2, c2 in itertools.product(range(ROWS), range(COLS)):
                if (r1, c1) == (r2, c2):
                    continue
                # i attacks j or j attacks i
                if fn_i(r1, c1, r2, c2) or fn_j(r2, c2, r1, c1):
                    forbidden.append((cell(r1, c1), cell(r2, c2)))

        if forbidden:
            # Add: NOT (pos[i] == ci AND pos[j] == cj) for each forbidden pair
            s.add(And([
                Not(And(pos[i] == ci, pos[j] == cj))
                for ci, cj in forbidden
            ]))

    # Enumerate all solutions
    solution_count = 0
    while s.check() == sat:
        m = s.model()
        sol = [m[pos[k]].as_long() for k in range(N)]
        solutions.append(sol)
        solution_count += 1

        # Block this solution (and symmetric duplicates via blocking exact assignment)
        s.add(Or([pos[k] != sol[k] for k in range(N)]))

        if solution_count % 10 == 0:
            print(f"  Found {solution_count} solutions so far...")

    return solutions

def print_board(sol):
    board = [["." for _ in range(COLS)] for _ in range(ROWS)]
    symbols = ["K", "Q", "B", "B", "N", "N", "R", "R"]
    for k, p in enumerate(sol):
        r, c = pos_to_rc(p)
        board[r][c] = symbols[k]
    print("  " + " ".join(str(c) for c in range(COLS)))
    for r in range(ROWS):
        print(f"{r} " + " ".join(board[r]))

def canonicalize(sol):
    """
    Produce a canonical form to deduplicate solutions where
    bishop1/bishop2, knight1/knight2, rook1/rook2 are interchangeable.
    Returns a frozenset-based key.
    """
    king_pos   = sol[0]
    queen_pos  = sol[1]
    bishops    = tuple(sorted([sol[2], sol[3]]))
    knights    = tuple(sorted([sol[4], sol[5]]))
    rooks      = tuple(sorted([sol[6], sol[7]]))
    return (king_pos, queen_pos, bishops, knights, rooks)

def main():
    print("Solving chess puzzle on 6×5 board...")
    print("Pieces: King, Queen, 2 Bishops (opposite colors), 2 Knights, 2 Rooks")
    print("Constraint: No piece attacks another\n")

    solutions = solve_all()

    # Deduplicate by canonical form
    seen = {}
    for sol in solutions:
        key = canonicalize(sol)
        if key not in seen:
            seen[key] = sol

    unique = list(seen.values())
    print(f"\nTotal raw solutions: {len(solutions)}")
    print(f"Unique solutions (deduplicating piece-pair swaps): {len(unique)}\n")

    for idx, sol in enumerate(unique, 1):
        print(f"── Solution {idx} ──")
        print_board(sol)
        labels = ["King", "Queen", "Bishop1", "Bishop2", "Knight1", "Knight2", "Rook1", "Rook2"]
        for k, p in enumerate(sol):
            r, c = pos_to_rc(p)
            col_name = "light" if color(r, c) == 0 else "dark"
            sq = f"({r},{c})"
            extra = f" [{col_name}]" if "Bishop" in labels[k] else ""
            print(f"  {labels[k]}: {sq}{extra}")
        print()

if __name__ == "__main__":
    main()

Related post: Lessons Learned With the Z3 SAT/SMT Solver

This time I asked Claude to formally prove the theorem from the previous post on partial fraction decomposition in an abstract setting. Unlike the previous experiments, I did not give it a proof or calculation to verify; I asked it to generate a proof.

This was the prompt:

Write a proof in Lean 4 for the following generalization of partial fraction decomposition.

If a ring R is a principle ideal domain (PID), then every element c of the field of fractions over R can be written in the form \[c = \sum_i \frac{a_i}{p_i^{r_i}}\]

where the p_i are nonassociate irreducible elements of R, the r_i are non-negative integers, and the elements a_i and p_i are relatively prime.

This was Claude’s immediate response:

I’ll work through this carefully, as it’s a substantial formalization task. Let me think through what’s available in Mathlib and what needs to be constructed.

This is a genuinely hard Lean 4 formalization problem. Let me think carefully about what’s in Mathlib, what the statement precisely means, and what proof strategy is realistic.

It also stated its overall proof strategy:

Proof strategy: Write c = a/b in lowest terms. Factor b = ∏ pᵢ^rᵢ. Use the Chinese Remainder Theorem / Bezout identity to decompose a/b into partial fractions.

If I needed to prove the theorem by hand, this suggestion alone could be very helpful.

The first attempt generated code that would not build. As before, a lot of the problems seem to stem from things moving around in Mathlib due to refactorings. There are also occasional hallucinations.

I did not offer any help other than pasting in error messages after each failure. When working on a real problem, I’d be more interactive. But as a test, I just passively pasted error messages and tried again. It took 11 iterations, but I finally got a proof. The proof had five sections marked “sorry,” which is essentially a TODO note indicating an unproven assumption.

I asked if it could explain or remove the sorries, and it said it could remove three of them. But the generated code did not build and I hit a session limit before I could debug the code. Here is the code with five sorry sections.

/-
  PartialFractions.lean  (v11 — final)
-/

import Mathlib

open UniqueFactorizationMonoid

variable {R : Type*} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]

structure PFDSummand (R : Type*) [CommRing R] where
  prime    : R
  exponent : ℕ
  numer    : R

noncomputable def PFDSummand.val [CommRing R] [IsDomain R] (s : PFDSummand R) :
    FractionRing R :=
  algebraMap R (FractionRing R) s.numer /
  algebraMap R (FractionRing R) (s.prime ^ s.exponent)

structure IsPFD [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
    (terms : List (PFDSummand R)) (c : FractionRing R) : Prop where
  irred    : ∀ s ∈ terms, Irreducible s.prime
  nonAssoc : ∀ s ∈ terms, ∀ t ∈ terms, s ≠ t → ¬Associated s.prime t.prime
  coprime  : ∀ s ∈ terms, IsCoprime s.numer s.prime
  sum_eq   : (terms.map PFDSummand.val).sum = c

private lemma algMap_ne_zero {a : R} (h : a ≠ 0) :
    (algebraMap R (FractionRing R)) a ≠ 0 :=
  map_ne_zero_iff _ (IsFractionRing.injective R (FractionRing R)) |>.mpr h

private lemma exists_num_denom (c : FractionRing R) :
    ∃ a b : R, b ≠ 0 ∧
      (algebraMap R (FractionRing R)) a / (algebraMap R (FractionRing R)) b = c := by
  obtain ⟨a, b, hb, hab⟩ := IsFractionRing.div_surjective (A := R) c
  exact ⟨a, b, nonZeroDivisors.ne_zero hb, hab⟩

-- ======================================================================
-- §6  Bézout splitting
-- ======================================================================

private lemma bezout_split (x y : R) (hcop : IsCoprime x y)
    (hx : x ≠ 0) (hy : y ≠ 0) (e : R) :
    ∃ s t : R, s * x + t * y = 1 ∧
      (algebraMap R (FractionRing R) e) /
        ((algebraMap R (FractionRing R) x) * (algebraMap R (FractionRing R) y)) =
      (algebraMap R (FractionRing R) (e * t)) / (algebraMap R (FractionRing R) x) +
      (algebraMap R (FractionRing R) (e * s)) / (algebraMap R (FractionRing R) y) := by
  obtain ⟨s, t, hst⟩ := hcop
  refine ⟨s, t, hst, ?_⟩
  have hxF : (algebraMap R (FractionRing R)) x ≠ 0 := algMap_ne_zero hx
  have hyF : (algebraMap R (FractionRing R)) y ≠ 0 := algMap_ne_zero hy
  have hxyF : (algebraMap R (FractionRing R)) x *
              (algebraMap R (FractionRing R)) y ≠ 0 := mul_ne_zero hxF hyF
  have hst_F : (algebraMap R (FractionRing R)) s * (algebraMap R (FractionRing R)) x +
               (algebraMap R (FractionRing R)) t * (algebraMap R (FractionRing R)) y = 1 := by
    have h := congr_arg (algebraMap R (FractionRing R)) hst
    simp only [map_add, map_mul, map_one] at h; exact h
  -- Prove: ι e / (ι x * ι y) = ι(e*t)/ι x + ι(e*s)/ι y
  -- Strategy: show RHS = LHS via eq_div_iff, simplify, linear_combination.
  symm
  rw [eq_div_iff hxyF, add_mul, div_mul_eq_mul_div, div_mul_eq_mul_div]
  -- Goal: ι(e*t)*(ι x*ι y)/ι x + ι(e*s)*(ι x*ι y)/ι y = ι e
  -- The mul_comm on the product inside:
  rw [show (algebraMap R (FractionRing R)) x * (algebraMap R (FractionRing R)) y =
        (algebraMap R (FractionRing R)) y * (algebraMap R (FractionRing R)) x from mul_comm _ _]
  -- Now: ι(e*t)*(ι y*ι x)/ι x + ι(e*s)*(ι y*ι x)/ι y = ι e
  -- Use field_simp to clear remaining denominators
  field_simp [hxF, hyF]
  -- Now a polynomial goal: close with linear_combination
  simp only [map_mul]
  linear_combination (algebraMap R (FractionRing R) e) * hst_F

-- ======================================================================
-- §7  Coprime numerator reduction
-- ======================================================================

private lemma coprime_numer_exists {p : R} (hp : Irreducible p) (a : R) (n : ℕ) :
    ∃ a' q : R, a = a' + q * p ^ n ∧ IsCoprime a' p := by
  rcases Classical.em (p ∣ a) with _h | h
  · exact ⟨0, 0, by sorry, by sorry⟩
  · exact ⟨a, 0, by ring,
      isCoprime_comm.mpr ((irreducible_iff_prime.mp hp).coprime_iff_not_dvd.mpr h)⟩

-- ======================================================================
-- §8  Main theorem
-- ======================================================================

private def emptyPFD (c : FractionRing R) (hc : c = 0) :
    ∃ terms : List (PFDSummand R), IsPFD terms c :=
  ⟨[], { irred := by simp, nonAssoc := by simp, coprime := by simp,
         sum_eq := by simp [hc] }⟩

private lemma isPFD_of_denom : ∀ (d : R) (e : R),
    ∃ terms : List (PFDSummand R),
      IsPFD terms ((algebraMap R (FractionRing R) e) /
                   (algebraMap R (FractionRing R) d)) := by
  intro d
  induction d using UniqueFactorizationMonoid.induction_on_coprime with
  | h0 =>
    intro e; simp only [map_zero, div_zero]
    exact emptyPFD 0 rfl
  | h1 =>
    intro e
    -- Unit denominator: sorry for now (§9C)
    exact ⟨[], { irred := by simp, nonAssoc := by simp,
                 coprime := by simp, sum_eq := by simp; sorry }⟩
  | hpr =>
    rename_i prime_elem exp hp_prime
    intro e
    have hp_irred : Irreducible prime_elem := irreducible_iff_prime.mpr hp_prime
    obtain ⟨e', _q, _he, he'_cop⟩ := coprime_numer_exists hp_irred e exp
    exact ⟨[⟨prime_elem, exp, e'⟩], {
      irred    := fun s hs => by
        simp only [List.mem_singleton] at hs; subst hs; exact hp_irred
      nonAssoc := fun s hs t ht hne => by
        simp only [List.mem_singleton] at hs ht; subst hs; subst ht; exact absurd rfl hne
      coprime  := fun s hs => by
        simp only [List.mem_singleton] at hs; subst hs; exact he'_cop
      sum_eq   := by
        simp only [List.map_singleton, List.sum_singleton, PFDSummand.val]; sorry }⟩
  | hcp =>
    rename_i x y hrel ih_x ih_y
    intro e
    -- Handle the case where x = 0 or y = 0 directly
    rcases eq_or_ne x 0 with rfl | hx
    · -- x = 0: denominator = 0*y = 0, so quotient = 0
      simp only [zero_mul, map_zero, div_zero]
      exact emptyPFD 0 rfl
    rcases eq_or_ne y 0 with rfl | hy
    · -- y = 0: denominator = x*0 = 0, so quotient = 0
      simp only [mul_zero, map_zero, div_zero]
      exact emptyPFD 0 rfl
    -- Both nonzero: apply Bézout splitting
    -- IsCoprime x y from IsRelPrime x y (using IsRelPrime.isCoprime)
    have hcop : IsCoprime x y := hrel.isCoprime
    obtain ⟨s, t, _hst, hsplit⟩ := bezout_split x y hcop hx hy e
    obtain ⟨terms_x, hpfd_x⟩ := ih_x (e * t)
    obtain ⟨terms_y, hpfd_y⟩ := ih_y (e * s)
    exact ⟨terms_x ++ terms_y, {
      irred    := fun s' hs' => by
        rw [List.mem_append] at hs'
        exact hs'.elim (hpfd_x.irred s') (hpfd_y.irred s')
      nonAssoc := fun s' hs' t' ht' hne => by
        rw [List.mem_append] at hs' ht'
        rcases hs' with hs' | hs' <;> rcases ht' with ht' | ht'
        · exact hpfd_x.nonAssoc s' hs' t' ht' hne
        · intro; sorry
        · intro; sorry
        · exact hpfd_y.nonAssoc s' hs' t' ht' hne
      coprime  := fun s' hs' => by
        rw [List.mem_append] at hs'
        exact hs'.elim (hpfd_x.coprime s') (hpfd_y.coprime s')
      sum_eq   := by
        rw [List.map_append, List.sum_append, hpfd_x.sum_eq, hpfd_y.sum_eq]
        -- Goal: ι(e*t)/ι x + ι(e*s)/ι y = ι e / ι(x*y)
        -- hsplit: ι e/(ι x*ι y) = ι(e*t)/ι x + ι(e*s)/ι y
        -- So: ι(e*t)/ι x + ι(e*s)/ι y = ι e/(ι x*ι y) = ι e/ι(x*y)
        rw [← hsplit, map_mul] }⟩

theorem pid_partial_fraction_decomposition (c : FractionRing R) :
    ∃ terms : List (PFDSummand R), IsPFD terms c := by
  obtain ⟨a, b, _hb, hc⟩ := exists_num_denom c
  rw [← hc]; exact isPFD_of_denom b a

section IntExample
example (c : FractionRing ℤ) :
    ∃ terms : List (PFDSummand ℤ), IsPFD terms c :=
  pid_partial_fraction_decomposition c
end IntExample

This post will look at partial fractions more generally.

Computation

Every polynomial with real coefficients can be factored into a product of linear and irreducible quadratic terms. But actually calculating this factorization is difficult if the degree of the denominator is large.

The quadratic equation is easy to use. There are analogs for 3rd and 4th order polynomials, but they’re cumbersome. And there is no formula in general for finding roots of polynomials of degree 5 or higher.

You could find the roots numerically, but if you’re going to go that route, maybe you should evaluate your integral numerically.

Still, it is useful in proving theorems to know that a partial fraction decomposition exists, even if in practice you cannot calculate it.

Complex numbers

Rational polynomials over the real numbers can be factored into powers of linear terms and irreducible quadratic terms. There are no irreducible quadratics over the complex numbers thanks to the Fundamental Theorem of Algebra, and every polynomial can be factored into a product of linear terms.

This means every rational in z can be broken into a sum of a polynomial in z and polynomials in 1/(z − z_i) where the z_i are the roots of the denominator. This fact is important, for example, in contour integration.

Principle ideal domains

The concept of partial fraction decomposition can be generalized to the field of fractions over a ring R [1].

If the ring R is a principle ideal domain (PID) [2], then every element c of the field K of fractions over R can be written in the form

where the p_i are nonassociate [3] irreducible elements of R, the r_i are non-negative integers, and the elements a_i and p_i are relatively prime.

When R is the ring of polynomials over a field, R is a PID, and the field of fractions is the set of rational functions over that field. When the field is the real or complex numbers, we get the results above. But the field could be something else, such as a finite field.

Integers

When R is the ring of integers, the irreducible elements are prime numbers. The nonassociate condition means you can’t count p and −p as distinct elements, so practically this means we only look at positive primes. The field of fractions is the rational numbers. So the theorem above says that every rational number can be written as a sum of fractions where the denominators of the fractions are prime powers and the numerators are relatively prime to the denominators.

The way you would decompose a rational number into fractions with prime power denominators is analogous to the way you’d do partial fraction decomposition in a calculus class. For example, suppose we want to decompose 46/75. The distinct prime factors of 75 are 3 and 5, and so we’d look for fractions with denominators 3, 5, and 25, and in fact

Footnotes

[1] The field of fractions over R is the set of formal terms a/b where a and b are in R and b ≠ 0. Operations are defined by analogy with rational numbers. If R is an integral domain, the field of fractions really is a field.

[2] A ring is a PID if every ideal can be generated by a single element.

[3] Two elements of an integral domain are said to be associate if they generate the same ideal.

A few weeks ago I wrote Pentagonal numbers are truncated triangular numbers. In a nutshell, if the pentagonal numbers are defined by

P_n = (3n² − n)/2

and the triangular numbers by

T_n = (n² + n)/2

then

P_n = T_{2n − 1} − T_{n − 1}.

Here’s a visualization of the equation.

Note that the equation asserts that two quadratic polynomials are equal. If the two polynomials are equal at three points, then they’re equal everywhere. We might as well make life easy and choose n = 0, 1, and 2.

If you’d like, you could do this in code.

>>> P = lambda n: (3*n**2 - n)/2
>>> T = lambda n: (n**2 + n)/2
>>> for n in [0, 1, 2]: assert(P(n) == T(2*n-1) - T(n-1))

This provides a rigorous proof, not just a sanity check.

Sometimes checking a few points is not enough to prove an equation with certainty, but it is enough to establish an equation with high probability. More on that here.

Related posts

• Testing pentagonal numbers
• Binomial coefficient trick

We have the formula

P_n = (3n² − n)/2

where n is a positive integer. If n is an integer but not positive, the equation above defines a generalized pentagonal number.

If you’re given an n, you can easily compute P_n. But suppose you’re given a large number x. How would you determine if it is a pentagonal number? And if it is a pentagonal number, how would you find n such that x = P_n?

Rejecting non-pentagonal numbers

If

x = P_n = (3n² − n)/2

then we can solve a quadratic equation for n:

n = (1 ± √(24x + 1))/6.

If 24x + 1 is not a perfect square, n is not an integer and x is not a pentagonal number, ordinary or generalized.

Small numbers

For example,

√(24 × 20260615 + 1)) = 22051.185…

and so 20260615 is not a pentagonal number nor a generalized pentagonal number.

Big numbers

Now suppose

x = 170141183460469231731687303715884105727.

Is this a pentagonal number? You can’t just compute √(24x + 1) in floating point arithmetic because the result is a 20-digit number, and floating point number have 15 digits of precision, so you can’t tell whether the result is an integer.

However, you can compute

⌊√(24x + 1)⌋

with only integer arithmetic using the sqrt_floor function from this post.

def sqrt_floor(n):
    a = n
    b = (n + 1) // 2
    while b < a:
        a = b
        b = (a*a + n) // (2*a)
    return a

The following prints a positive number,

x = 2**127 - 1
y = 24*x + 1
r = sqrt_floor(y)
print(y - r**2)

which tells us y is not a perfect square.

Finding the index

Now suppose y is a perfect square. Then the roots of

(1 ± √(24x + 1))/6

are rational, but are they integers? In fact one, and only one, of the roots will be an integer. If

24x + 1 = r²

then r is congruent to ±1 mod 6 because the left side is congruent to 1 mod 6. If r = 1 mod 6 then the smaller root is an integer, and if r = 5 mod 6 then the larger root is an integer.

So if 24x + 1 = r², then x is a pentagonal number if r = 5 mod 6 and a generalized pentagonal number otherwise.

The function pentagonal_index takes a number x and return n if x = P_n and None if no such n exists.

def pentagonal_index(x):
    y = 24*x + 1
    r = sqrt_floor(y)
    if r*r != y:
        return None
    if r % 6 == 5:
        return (1 + r) // 6
    else:
        return (1 - r) // 6

We can test this with the following code.

P = lambda n: (3*n**2 - n) // 2
for n in [2, 3, -4, -5, 10**200]:
    assert(pentagonal_index(P(n)) == n)

Integer division in Python

Note that P(10**200) is too big to fit into a float, but the code works fine. This is because we use integer division (//) everywhere. If we had said

P = lambda n: (3*n**2 - n) / 2

the test above would pass for the small values of n but output

OverflowError: integer division result too large for a float

when it came to n = 10²⁰⁰.

Related posts

• Partitions and pentagons
• Certified Fibonacci numbers
• Truncated triangular numbers

Write Lean code to verify the two theorems at the top of this post:
https://www.johndcook.com/blog/2025/05/07/quaternions-and-rotation-matrices/

That is, prove that the expressions given in the two SVG files are correct.

The post included Python code to numerically verify the equations. However, the Python code differed from the LaTeX code for the image in one subscript [2]. Although I asked Claude to prove the expressions in the SVG file produced by the LaTeX code, it detected the conflict between the Python and LaTeX and correctly concluded that the former was correct.

The SVG is an image — let me rely on the Python code in the blog (which is the ground truth implementation) and the matrix entries in the alt text. … Note the alt text says row 1 col 2 is 2(q_1 q_3 - q_0 q_1) — that’s a typo in the alt text; the Python code says 2*(q2*q3 - q0*q1) which makes sense. I’ll use the Python code as the authoritative source.

The code did not run on first attempt. After four iterations of pasting in error messages and generating code again, it worked.

Here is the final Lean 4 code.

/-
  Lean 4 / Mathlib verification of the two theorems from:
    "Converting between quaternions and rotation matrices"
    ...

  Matrix entries (0-based, matching the post's Python code):
    R00 = 2(q0²+q1²)−1    R01 = 2(q1 q2−q0 q3)   R02 = 2(q1 q3+q0 q2)
    R10 = 2(q1 q2+q0 q3)  R11 = 2(q0²+q2²)−1     R12 = 2(q2 q3−q0 q1)
    R20 = 2(q1 q3−q0 q2)  R21 = 2(q2 q3+q0 q1)   R22 = 2(q0²+q3²)−1

  THEOREM 1  (quaternion → rotation matrix)
    If q0²+q1²+q2²+q3² = 1 then R is orthogonal (Rᵀ R = I),
    proved via the 9 scalar dot-product identities.

  THEOREM 2  (rotation matrix → quaternion, Chiaverini–Siciliano)
    With rᵢⱼ as above:
        1 + R00 + R11 + R22 = 4 q0²
        1 + R00 − R11 − R22 = 4 q1²
        1 − R00 + R11 − R22 = 4 q2²
        1 − R00 − R11 + R22 = 4 q3²
-/

import Mathlib.Tactic

set_option linter.style.whitespace false

variable (q0 q1 q2 q3 : ℝ)

/-! ## Theorem 1 : Rᵀ R = I -/

-- ── Column norms = 1 ─────────────────────────────────────────────────────────

theorem col0_norm (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q0 ^ 2 + q1 ^ 2) - 1) ^ 2 + (2 * (q1 * q2 + q0 * q3)) ^ 2 +
    (2 * (q1 * q3 - q0 * q2)) ^ 2 = 1 := by
  nlinarith [sq_nonneg (q0 ^ 2 + q1 ^ 2 - q2 ^ 2 - q3 ^ 2),
             sq_nonneg (q0 * q2 + q1 * q3), sq_nonneg (q0 * q3 - q1 * q2),
             sq_nonneg q0, sq_nonneg q1, sq_nonneg q2, sq_nonneg q3]

theorem col1_norm (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q1 * q2 - q0 * q3)) ^ 2 + (2 * (q0 ^ 2 + q2 ^ 2) - 1) ^ 2 +
    (2 * (q2 * q3 + q0 * q1)) ^ 2 = 1 := by
  nlinarith [sq_nonneg (q0 ^ 2 - q1 ^ 2 + q2 ^ 2 - q3 ^ 2),
             sq_nonneg (q0 * q1 + q2 * q3), sq_nonneg (q0 * q3 - q1 * q2),
             sq_nonneg q0, sq_nonneg q1, sq_nonneg q2, sq_nonneg q3]

theorem col2_norm (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q1 * q3 + q0 * q2)) ^ 2 + (2 * (q2 * q3 - q0 * q1)) ^ 2 +
    (2 * (q0 ^ 2 + q3 ^ 2) - 1) ^ 2 = 1 := by
  nlinarith [sq_nonneg (q0 ^ 2 - q1 ^ 2 - q2 ^ 2 + q3 ^ 2),
             sq_nonneg (q0 * q1 - q2 * q3), sq_nonneg (q0 * q2 + q1 * q3),
             sq_nonneg q0, sq_nonneg q1, sq_nonneg q2, sq_nonneg q3]

-- ── Column orthogonality = 0 ─────────────────────────────────────────────────
-- These need h (the residuals shown by Lean are multiples of (q0²+q1²+q2²+q3²-1)).
-- We use linear_combination with the explicit witnesses.

theorem col0_col1_orth (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q0 ^ 2 + q1 ^ 2) - 1) * (2 * (q1 * q2 - q0 * q3)) +
    (2 * (q1 * q2 + q0 * q3)) * (2 * (q0 ^ 2 + q2 ^ 2) - 1) +
    (2 * (q1 * q3 - q0 * q2)) * (2 * (q2 * q3 + q0 * q1)) = 0 := by
  linear_combination 4 * q1 * q2 * h

theorem col0_col2_orth (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q0 ^ 2 + q1 ^ 2) - 1) * (2 * (q1 * q3 + q0 * q2)) +
    (2 * (q1 * q2 + q0 * q3)) * (2 * (q2 * q3 - q0 * q1)) +
    (2 * (q1 * q3 - q0 * q2)) * (2 * (q0 ^ 2 + q3 ^ 2) - 1) = 0 := by
  linear_combination 4 * q1 * q3 * h

theorem col1_col2_orth (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q1 * q2 - q0 * q3)) * (2 * (q1 * q3 + q0 * q2)) +
    (2 * (q0 ^ 2 + q2 ^ 2) - 1) * (2 * (q2 * q3 - q0 * q1)) +
    (2 * (q2 * q3 + q0 * q1)) * (2 * (q0 ^ 2 + q3 ^ 2) - 1) = 0 := by
  linear_combination 4 * q2 * q3 * h

-- ── Row norms = 1 ────────────────────────────────────────────────────────────

theorem row0_norm (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q0 ^ 2 + q1 ^ 2) - 1) ^ 2 + (2 * (q1 * q2 - q0 * q3)) ^ 2 +
    (2 * (q1 * q3 + q0 * q2)) ^ 2 = 1 := by
  nlinarith [sq_nonneg (q0 ^ 2 + q1 ^ 2 - q2 ^ 2 - q3 ^ 2),
             sq_nonneg (q0 * q2 - q1 * q3), sq_nonneg (q0 * q3 + q1 * q2),
             sq_nonneg q0, sq_nonneg q1, sq_nonneg q2, sq_nonneg q3]

theorem row1_norm (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q1 * q2 + q0 * q3)) ^ 2 + (2 * (q0 ^ 2 + q2 ^ 2) - 1) ^ 2 +
    (2 * (q2 * q3 - q0 * q1)) ^ 2 = 1 := by
  nlinarith [sq_nonneg (q0 ^ 2 - q1 ^ 2 + q2 ^ 2 - q3 ^ 2),
             sq_nonneg (q0 * q1 - q2 * q3), sq_nonneg (q0 * q3 + q1 * q2),
             sq_nonneg q0, sq_nonneg q1, sq_nonneg q2, sq_nonneg q3]

theorem row2_norm (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q1 * q3 - q0 * q2)) ^ 2 + (2 * (q2 * q3 + q0 * q1)) ^ 2 +
    (2 * (q0 ^ 2 + q3 ^ 2) - 1) ^ 2 = 1 := by
  nlinarith [sq_nonneg (q0 ^ 2 - q1 ^ 2 - q2 ^ 2 + q3 ^ 2),
             sq_nonneg (q0 * q1 + q2 * q3), sq_nonneg (q0 * q2 - q1 * q3),
             sq_nonneg q0, sq_nonneg q1, sq_nonneg q2, sq_nonneg q3]

-- ── Row orthogonality = 0 ────────────────────────────────────────────────────

theorem row0_row1_orth (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q0 ^ 2 + q1 ^ 2) - 1) * (2 * (q1 * q2 + q0 * q3)) +
    (2 * (q1 * q2 - q0 * q3)) * (2 * (q0 ^ 2 + q2 ^ 2) - 1) +
    (2 * (q1 * q3 + q0 * q2)) * (2 * (q2 * q3 - q0 * q1)) = 0 := by
  linear_combination 4 * q1 * q2 * h

theorem row0_row2_orth (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q0 ^ 2 + q1 ^ 2) - 1) * (2 * (q1 * q3 - q0 * q2)) +
    (2 * (q1 * q2 - q0 * q3)) * (2 * (q2 * q3 + q0 * q1)) +
    (2 * (q1 * q3 + q0 * q2)) * (2 * (q0 ^ 2 + q3 ^ 2) - 1) = 0 := by
  linear_combination 4 * q1 * q3 * h

theorem row1_row2_orth (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    (2 * (q1 * q2 + q0 * q3)) * (2 * (q1 * q3 - q0 * q2)) +
    (2 * (q0 ^ 2 + q2 ^ 2) - 1) * (2 * (q2 * q3 + q0 * q1)) +
    (2 * (q2 * q3 - q0 * q1)) * (2 * (q0 ^ 2 + q3 ^ 2) - 1) = 0 := by
  linear_combination 4 * q2 * q3 * h

/-! ## Theorem 2 : Chiaverini–Siciliano square-root arguments -/

theorem cs_arg0 (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    1 + (2 * (q0 ^ 2 + q1 ^ 2) - 1) + (2 * (q0 ^ 2 + q2 ^ 2) - 1) +
    (2 * (q0 ^ 2 + q3 ^ 2) - 1) = 4 * q0 ^ 2 := by linarith

theorem cs_arg1 (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    1 + (2 * (q0 ^ 2 + q1 ^ 2) - 1) - (2 * (q0 ^ 2 + q2 ^ 2) - 1) -
    (2 * (q0 ^ 2 + q3 ^ 2) - 1) = 4 * q1 ^ 2 := by linarith

theorem cs_arg2 (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    1 - (2 * (q0 ^ 2 + q1 ^ 2) - 1) + (2 * (q0 ^ 2 + q2 ^ 2) - 1) -
    (2 * (q0 ^ 2 + q3 ^ 2) - 1) = 4 * q2 ^ 2 := by linarith

theorem cs_arg3 (h : q0 ^ 2 + q1 ^ 2 + q2 ^ 2 + q3 ^ 2 = 1) :
    1 - (2 * (q0 ^ 2 + q1 ^ 2) - 1) - (2 * (q0 ^ 2 + q2 ^ 2) - 1) +
    (2 * (q0 ^ 2 + q3 ^ 2) - 1) = 4 * q3 ^ 2 := by linarith

/-! ### Sign-correction identities (pure ring) -/

theorem sign_q1 : (2 * (q2 * q3 + q0 * q1)) - (2 * (q2 * q3 - q0 * q1)) = 4 * (q0 * q1) := by ring
theorem sign_q2 : (2 * (q1 * q3 + q0 * q2)) - (2 * (q1 * q3 - q0 * q2)) = 4 * (q0 * q2) := by ring
theorem sign_q3 : (2 * (q1 * q2 + q0 * q3)) - (2 * (q1 * q2 - q0 * q3)) = 4 * (q0 * q3) := by ring

[1] I very much appreciate error reports. Thank you to everyone who has helped improve this blog.

[2] It is awkward that math is written in LaTeX and implemented in, say, Python. Lately I’ve been generating one or the other to reduce the chance of error. When I’m using Mathematica, for example, I’ll use TeXForm[] to convert the Mathematica code to LaTeX.

Of course there’s not a lot of market demand for solving chess puzzles, but there is demand for solving real-world problems that amount to logic puzzles. Experiments with chess puzzles suggest writing Prolog with LLM help might be pleasant. The syntax of Prolog can be a little odd, but the LLM handles that. And because Prolog has been around so long without changing much, you’d expect LLMs to be good at generating code in it. [1]

I gave ChatGPT this prompt:

Write a SWI Prolog program to solve the following chess puzzle. Place a queen, king, rook, bishop, and knight on a 4 by 4 chessboard so no piece attacks another. Print all solutions.

It produced a file chess4.pl (below) that I ran with

swipl -q -s chess4.pl -g solve -t halt

It found all 16 solutions:

Solution 1:
  queen=1-2  king=2-4  rook=3-1  bishop=4-3  knight=4-4
. K . N
. . . B
Q . . .
. . R .

Solution 2:
  queen=1-2  king=4-3  rook=2-4  bishop=3-1  knight=4-1
. R . .
. . . K
Q . . .
. . B N

...

Here’s the code.

% chess4.pl
% Place queen, king, rook, bishop, and knight on a 4x4 board
% so that no piece attacks another.

:- use_module(library(lists)).

square(X-Y) :-
    between(1, 4, X),
    between(1, 4, Y).

solve :-
    findall(Board, solution(Board), Boards),
    print_solutions(Boards, 1),
    length(Boards, Count),
    format('Total solutions: ~d~n', [Count]).

solution(Board) :-
    Pieces = [queen, king, rook, bishop, knight],
    findall(S, square(S), Squares),
    place_pieces(Pieces, Squares, Board),
    safe(Board).

place_pieces([], _, []).
place_pieces([Piece | Pieces], Squares, [Piece-Square | Board]) :-
    select(Square, Squares, RemainingSquares),
    place_pieces(Pieces, RemainingSquares, Board).

safe(Board) :-
    safe(Board, Board).

safe([], _).
safe([Piece-Square | Rest], Board) :-
    forall(
        member(OtherPiece-OtherSquare, Rest),
        non_attacking(Piece-Square, OtherPiece-OtherSquare, Board)
    ),
    safe(Rest, Board).

non_attacking(P1-S1, P2-S2, Board) :-
    \+ attacks(P1, S1, S2, Board),
    \+ attacks(P2, S2, S1, Board).

% Attack rules

attacks(king, X1-Y1, X2-Y2, _) :-
    X1-Y1 \= X2-Y2,
    DX is abs(X1 - X2),
    DY is abs(Y1 - Y2),
    DX =< 1,
    DY =< 1. attacks(knight, X1-Y1, X2-Y2, _) :- DX is abs(X1 - X2), DY is abs(Y1 - Y2), ( DX =:= 1, DY =:= 2 ; DX =:= 2, DY =:= 1 ). attacks(rook, S1, S2, Board) :- same_rank_or_file(S1, S2), clear_line(S1, S2, Board). attacks(bishop, S1, S2, Board) :- same_diagonal(S1, S2), clear_line(S1, S2, Board). attacks(queen, S1, S2, Board) :- ( same_rank_or_file(S1, S2) ; same_diagonal(S1, S2) ), clear_line(S1, S2, Board). same_rank_or_file(X1-Y1, X2-Y2) :- ( X1 =:= X2 ; Y1 =:= Y2 ). same_diagonal(X1-Y1, X2-Y2) :- DX is abs(X1 - X2), DY is abs(Y1 - Y2), DX =:= DY. % For sliding pieces, make sure no piece blocks the path. clear_line(X1-Y1, X2-Y2, Board) :- step(X1, X2, SX), step(Y1, Y2, SY), NX is X1 + SX, NY is Y1 + SY, clear_path(NX-NY, X2-Y2, SX-SY, Board). clear_path(Target, Target, _, _) :- !. clear_path(X-Y, Target, SX-SY, Board) :- \+ occupied(X-Y, Board), NX is X + SX, NY is Y + SY, clear_path(NX-NY, Target, SX-SY, Board). step(A, B, 0) :- A =:= B. step(A, B, 1) :- B > A.
step(A, B, -1) :-
    B < A.

occupied(Square, Board) :-
    member(_-Square, Board).

% Printing

print_solutions([], _).
print_solutions([Board | Rest], N) :-
    format('Solution ~d:~n', [N]),
    print_coordinates(Board),
    print_board(Board),
    nl,
    N1 is N + 1,
    print_solutions(Rest, N1).

print_coordinates(Board) :-
    member(queen-Q, Board),
    member(king-K, Board),
    member(rook-R, Board),
    member(bishop-B, Board),
    member(knight-N, Board),
    format('  queen=~w  king=~w  rook=~w  bishop=~w  knight=~w~n',
           [Q, K, R, B, N]).

print_board(Board) :-
    forall(
        between(1, 4, Row0),
        (
            Y is 5 - Row0,
            forall(
                between(1, 4, X),
                (
                    piece_at(X-Y, Board, Symbol),
                    format('~w ', [Symbol])
                )
            ),
            nl
        )
    ).

piece_at(Square, Board, Symbol) :-
    member(Piece-Square, Board),
    !,
    piece_symbol(Piece, Symbol).
piece_at(_, _, '.').

piece_symbol(queen,  'Q').
piece_symbol(king,   'K').
piece_symbol(rook,   'R').
piece_symbol(bishop, 'B').
piece_symbol(knight, 'N').

[1] I’ve played around with generating Prolog and Lean this weekend, and I’ve had better results with Prolog. The problems with Lean haven’t been Lean per se but the Mathlib library. The library is frequently refactored, which makes sense for a young language, but this makes it harder to generate and debug code.

The code was also printed on T-shirts. The shirt was classified as munitions because it contained source code for strong encryption. More on the shirt here.

This was the code:

#!/bin/perl -s-- -export-a-crypto-system-sig -RSA-3-lines-PERL
$m=unpack(H.$w,$m."\0"x$w),$_=`echo "16do$w 2+4Oi0$d*-^1[d2%Sa
2/d0<X+d*La1=z\U$n%0]SX$k"[$m*]\EszlXx++p|dc`,s/^.|\W//g,print
pack('H*',$_)while read(STDIN,$m,($w=2*$d-1+length$n&~1)/2)

My initial intention was to unpack the code, explaining each piece in detail. I don’t have the time or patience for that, and I imagine many readers don’t either. For more of a blow-by-blow explanation, see this commentary from 1995.

dc

In the middle of the code is

    echo ... | dc

This is the most dense and most important part of the code. Perl calls the dc calculator to do the arbitrary precision arithmetic that RSA encryption requires.

I’ve written about bc several times. bc (“basic calculator”) was a originally a more user-friendly wrapper around the reverse-Polish dc (“desktop calculator”). dc is still part of every Unix and Unix-like system, but I imagine bc is far more popular.

The important feature of dc for this post is that it is stack-based, meaning that users would push data and commands on to the stack and pop results off the stack. A sequence of commands that might be understandable when interactively using dc would look cryptic in a transcript. This is part of what makes the code so cryptic.

I’ll parse just a tiny bit of the dc code to give a flavor of what it does. The first four characters 16do instructs dc to push 16 on to the stack, duplicate it, and set the output radix to 16, i.e. these four characters tell dc to work in hexadecimal.

Believe it or not, the dc code is computing

m^k mod n

using fast exponentiation, which is the key step in the RSA algorithm.

Textbook RSA

Note that Adam Back’s code is computing what we would now call textbook RSA, not RSA as it has been refined over the years and is currently implemented.

Related posts

• Martin Gardner’s RSA article
• RSA encryption flaws
• Three applications of Euler’s theorem