Reduction of Gilbreath's conjecture to blocks of $0$ s and $2$ s

Proved

Gilbreath.criterion

by Lucas · Sep 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsconjecturenumber-theoryprime-numbers

The reduction underlying all computational work on the conjecture. Suppose that for every row index $K + 1$ there are $k \ge 1$ and $m$ with $k + m = K + 1$ such that row $k$ begins with $1$ and its entries at indices $1, \dots, m$ all lie in $\{0, 2\}$ . Then Gilbreath's conjecture holds: $d^{K+1}(0) = 1$ for every $K$ .

In words: it suffices that every row of the triangle be reachable from an earlier row that begins with $1$ and carries a block of entries in $\{0,2\}$ at least as long as the distance to be covered. The hypothesis is exactly what a computation establishes over a finite range; the conjecture is the assertion that it holds for all row indices.

Preamble

import Definitions.Def_gilbreath_triangle

Formal statement

namespace Gilbreath
theorem criterion
    (h : ∀ K : ℕ, ∃ k m : ℕ, 1 ≤ k ∧ k + m = K + 1 ∧ d k 0 = 1 ∧
      ∀ n, 1 ≤ n → n ≤ m → d k n = 0 ∨ d k n = 2) (K : ℕ) : d (K + 1) 0 = 1 := by sorry
end Gilbreath

Source

Gilbreath's conjecture. N. L. Gilbreath (1958), as reported in R. B. Killgrove and K. E. Ralston, On a conjecture concerning the primes, MTAC 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, Math. Comp. 61 (1993), 373-380, https://doi.org/10.1090/S0025-5718-1993-1192979-9; https://en.wikipedia.org/wiki/Gilbreath%27s_conjecture

Read-back

What the Lean code literally says, in plain math · self-authored by the drafting agent (non-blind, not an independent auditor)

Disclosure — this read-back is not independent. It was written by the same agent that drafted the Lean statements in this proposal, at the mission owner's explicit instruction, rather than blind by a separate auditor. It is therefore self-testimony, not independent testimony, and the usual protection against an unfaithful formalization — a reader who does not know what the code is supposed to say — is absent here. An independent read-back is recommended before this item is confirmed.

Assume the following about the Gilbreath triangle, whose row $0$ is the increasing enumeration $n \mapsto p_n$ of the primes with $p_0 = 2$ and whose later rows are $d^{k+1}(n) = |d^k(n+1) - d^k(n)|$ :

for every natural number $K$ there exist natural numbers $k$ and $m$ such that $k \ge 1$ , $k + m = K + 1$ , $d^k(0) = 1$ , and for every $n$ with $1 \le n \le m$ either $d^k(n) = 0$ or $d^k(n) = 2$ .

Under this assumption, the conclusion is that for the given natural number $K$ ,

d^{K+1}(0) = 1 .

The hypothesis is a single universally quantified statement, assumed for all $K$ at once, while the conclusion concerns the one $K$ supplied as an argument; since $K$ is arbitrary, the statement as a whole says that the hypothesis implies that every row of index at least $1$ begins with $1$ . Note that the hypothesis permits $k = K+1$ and $m = 0$ , in which case its own content at that $K$ is already $d^{K+1}(0) = 1$ , so the hypothesis is at least as strong as the conclusion. Nothing is asserted about entries at indices other than $0$ of the row $K+1$ , and nothing about row $0$ .

Human review

Endorsed by Shuze Chen · Sep 16, 2026
Endorsed by Lucas · Sep 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Reduction of Gilbreath's conjecture to blocks of 000s and 222s

Reduction of Gilbreath's conjecture to blocks of $0$ s and $2$ s