Rows $1$ to $4$ of the Gilbreath triangle begin with $1$

Proved

Gilbreath.small_rows

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

combinatoricsconjecturenumber-theoryprime-numbers

A finite verification of Gilbreath's conjecture for the first four rows: for $1 \le k \le 4$ the leading entry $d^k(0)$ of row $k$ of the Gilbreath triangle equals $1$ . Only the primes $p_0, \dots, p_4 = 2, 3, 5, 7, 11$ are involved, since the leading entry of row $k$ depends on the first $k+1$ entries of row $0$ .

Preamble

import Definitions.Def_gilbreath_triangle

Formal statement

namespace Gilbreath
theorem small_rows (k : ℕ) (hk : 1 ≤ k) (hk' : k ≤ 4) : d k 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.

For every natural number $k$ satisfying both $1 \le k$ and $k \le 4$ , the value at index $0$ of the $k$ -th row of the Gilbreath triangle equals $1$ :

1 \le k \le 4 \ \Longrightarrow\ d^k(0) = 1.

Here $d^0$ is the sequence $n \mapsto p_n$ of all primes in increasing order starting at $p_0 = 2$ , and $d^{k+1}(n) = |d^k(n+1) - d^k(n)|$ , the absolute difference of consecutive entries of the previous row. The two hypotheses are given as separate assumptions on $k$ ; the statement says nothing about $k = 0$ (where the value would be $p_0 = 2$ ) and nothing about any $k \ge 5$ . It asserts only the value at index $0$ , not at any later index of those rows. The hypotheses are satisfiable (for example by $k = 1$ ), so the claim is not vacuous.

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

Rows 111 to 444 of the Gilbreath triangle begin with 111

Rows $1$ to $4$ of the Gilbreath triangle begin with $1$