Motivation

Write the primes in increasing order, take the absolute differences of consecutive entries, take the absolute differences of the resulting row, and repeat. Every row produced this way appears to begin with $1$:

$$\begin{array}{llllllll} 2 & 3 & 5 & 7 & 11 & 13 & 17 & \dots\\ 1 & 2 & 2 & 4 & 2 & 4 & \dots\\ 1 & 0 & 2 & 2 & 2 & \dots\\ 1 & 2 & 0 & 0 & \dots\\ 1 & 2 & 0 & \dots \end{array}$$

Gilbreath's conjecture asserts that this never fails. The observation is due to Norman L. Gilbreath (1958), who rediscovered a statement already published by François Proth in 1878 together with an argument that is not accepted as a proof. It is attractive because it is elementary to state and because it is one of the few statements about the primes whose difficulty is not visibly analytic: it concerns the combinatorics of iterated differences rather than the distribution of primes directly.

Timeline.

• 1878 — Proth states the property and publishes a proof that is now regarded as erroneous.
• 1958 — Gilbreath rediscovers the pattern; it circulates as a conjecture.
• 1959 — Killgrove and Ralston verify the leading entry for the first $63{,}418$ rows (MTAC 13 (1959), 121–122).
• 1993 — Odlyzko reports a verification of the leading entry for all rows of index at most $\pi(10^{13}) \approx 3.4 \times 10^{11}$, using an argument that propagates a long block of entries lying in $\{0,2\}$ downwards through the triangle (Math. Comp. 61 (1993), 373–380).

No proof is known.

Setting

Let $p_0 = 2 < p_1 = 3 < p_2 = 5 < \dots$ be the increasing enumeration of the prime numbers, indexed from $0$. Define the rows of the Gilbreath triangle by

$$d^0(n) = p_n, \qquad d^{k+1}(n) = \bigl| d^{k}(n+1) - d^{k}(n) \bigr| \quad (k, n \ge 0).$$

Thus $d^k$ is an infinite sequence of natural numbers for every $k$, row $0$ is the sequence of primes, row $1$ is the sequence of prime gaps $p_{n+1}-p_n$, and each later row is the sequence of absolute differences of consecutive entries of the row above it. Only the leading entry $d^k(0)$ of each row is at issue.

More generally, for an arbitrary sequence $a : \mathbb{N} \to \mathbb{N}$ write $(\Delta a)(n) = |a(n+1) - a(n)|$ and $\Delta^j a$ for the $j$-fold iterate, so that $d^k = \Delta^k p$.

Formalization targets

Goal

$$\forall k \ge 1,\qquad d^{k}(0) = 1 .$$

This is the conjecture in its standard form: every row after the row of primes begins with $1$. It fixes no constants and no ranges, so no computational advance can invalidate it.

Milestones

The milestone list collects the statements that a proof, or a further computational verification, would be built from: the two low-level structural facts about the triangle (row $1$ is the gap sequence; from row $1$ on, the leading entry is odd and all later entries are even), a finite verification of the first rows, and the two statements underlying Odlyzko's method — the propagation lemma for an arbitrary sequence beginning $1$ and continuing in $\{0,2\}$, and the reduction of the conjecture to the existence, for each row index, of an earlier row with a long enough block of entries in $\{0,2\}$.

Significance

The result itself. The conjecture is not known to imply other open statements about the primes, and its interest lies elsewhere: it is a test case for how much of the fine structure of the prime sequence is forced by coarse information. The propagation mechanism shows that the conjecture for a given row index follows from purely local data about an earlier row, and that mechanism is what every verification to date has relied on. A proof would have to show that such blocks of entries in $\{0,2\}$ always appear early enough, which is a statement about the density of small prime gaps in disguise.

Formalizing it. Nothing here is currently formalized: Mathlib has the prime enumeration $n \mapsto p_n$ (Nat.nth Nat.Prime) and the basic facts about it, but not the iterated-difference triangle nor any of its properties. This mission contributes the definition of the triangle, the structural facts about its rows, and a machine-checked version of the reduction step that all computational work on the problem uses. The goal theorem itself is open — the milestones are known mathematics, and each is provable with current tools, while the goal is not.

Difficulty

The obvious attack is induction on the row index: to see that $d^{k+1}(0) = 1$ it suffices to know that $d^{k}(0) = 1$ and $d^{k}(1) \in \{0,2\}$. But controlling $d^{k}(1)$ requires controlling $d^{k-1}(1)$ and $d^{k-1}(2)$, and so on: the invariant that closes is not "the row begins with $1$" but "the row begins with $1$ and its next $m$ entries lie in $\{0,2\}$", and each application of the difference operator consumes one entry of that block. So a finite block of good entries only carries the conclusion a finite number of rows further down, and the conjecture needs such blocks to keep reappearing forever, arbitrarily far down the triangle. Nothing is known that produces them.

A second warning, due to Hallard Croft: the property is not specific to the primes. Sequences that start with $2$, continue with odd numbers, and have gaps that are not too large empirically exhibit the same behaviour, so any proof that uses only such coarse features would prove a much more general statement — and conversely, an argument exploiting deep properties of primes is likely to be proving the wrong thing.

Formalization scope

Rows are total functions $\mathbb{N} \to \mathbb{N}$, defined for every index, and the whole triangle is a single family indexed by the row number. Differences are taken as Int.natAbs of a difference computed in $\mathbb{Z}$, so truncated natural subtraction never occurs; the one place where $\mathbb{N}$-subtraction does appear is the milestone identifying row $1$ with the gap sequence, where the subtraction is justified by monotonicity of $n \mapsto p_n$.

Primes are indexed from $0$ via Mathlib's Nat.nth Nat.Prime, so $p_0 = 2$; rows are indexed with row $0$ the primes, and the goal quantifies over all $k \ge 1$ in the form d (k + 1) 0 = 1, with no upper bound and no extra hypothesis, so no vacuous or finitely-truncated reading of the goal is available. The general difference operator is stated for arbitrary sequences $\mathbb{N} \to \mathbb{N}$, which is what makes the propagation lemma usable as a black box, and reusable beyond this mission.

A complete development needs no analytic input for the milestones: Mathlib's Nat.nth, Nat.prime_nth_prime, Nat.nth_prime_zero_eq_two and the strict monotonicity of the prime enumeration suffice. Contributions that would extend the mission beyond its current list: a formal version of a concrete computational verification (checking that the leading entries of the first $N$ rows are $1$ for an $N$ well beyond the hand-checkable range), and formalizations of the general statement for non-prime sequences of the Croft type.

Selected references

• N. L. Gilbreath, as reported in R. B. Killgrove and K. E. Ralston, On a conjecture concerning the primes, Mathematical Tables and Other Aids to Computation 13 (1959), 121–122. https://doi.org/10.1090/S0025-5718-1959-0105398-3
• A. M. Odlyzko, Iterated absolute values of differences of consecutive primes, Mathematics of Computation 61 (1993), 373–380. https://doi.org/10.1090/S0025-5718-1993-1192979-9
• Gilbreath's conjecture, Wikipedia. https://en.wikipedia.org/wiki/Gilbreath%27s_conjecture