Every row after the primes starts odd and continues even

Proved

Gilbreath.head_odd_tail_even

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

combinatoricsconjecturenumber-theoryprime-numbers

Parity structure of the Gilbreath triangle: for every $k \ge 1$ the leading entry $d^k(0)$ is odd and every later entry $d^k(n)$ , $n \ge 1$ , is even. The reason is that $p_0 = 2$ is the only even prime, so row $1$ starts with the odd number $1$ and continues with even gaps, and this parity pattern is reproduced by taking differences. In particular the leading entry of every row after the first is odd, hence nonzero — the conjecture is exactly the assertion that it is never larger than $1$ .

Preamble

import Definitions.Def_gilbreath_triangle

Formal statement

namespace Gilbreath
theorem head_odd_tail_even (k : ℕ) :
    Odd (d (k + 1) 0) ∧ ∀ n : ℕ, Even (d (k + 1) (n + 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$ , two things hold simultaneously about row $k+1$ of the Gilbreath triangle:

its entry at index $0$ is odd, i.e. $d^{k+1}(0) = 2m+1$ for some natural $m$ ; and
for every natural number $n$ , its entry at index $n+1$ is even, i.e. $d^{k+1}(n+1)$ is twice a natural number.

Row $0$ is the increasing enumeration $n \mapsto p_n$ of the primes with $p_0 = 2$ , and $d^{k+1}(n) = |d^k(n+1) - d^k(n)|$ . The quantifier over $k$ is unrestricted, so the claim covers every row of index at least $1$ ; it says nothing about row $0$ . Because indices are written as $n+1$ , the second part covers exactly the entries at indices $1, 2, 3, \dots$ and excludes index $0$ . No hypotheses are imposed. Note that $0$ counts as even here and that oddness of $d^{k+1}(0)$ entails $d^{k+1}(0) \ge 1$ , but no upper bound on any entry is asserted.

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