Row $1$ is the sequence of prime gaps

Proved

Gilbreath.row_one_eq_prime_gap

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

combinatoricsconjecturenumber-theoryprime-numbers

The first row of the Gilbreath triangle is the sequence of prime gaps: $d^1(n) = p_{n+1} - p_n$ for every $n \ge 0$ . The right-hand side is a subtraction of natural numbers, which is legitimate here because the enumeration of the primes is strictly increasing, so the absolute value in the definition of the triangle can be dropped at this level.

Preamble

import Definitions.Def_gilbreath_triangle

Formal statement

namespace Gilbreath
theorem row_one_eq_prime_gap (n : ℕ) :
    d 1 n = Nat.nth Nat.Prime (n + 1) - Nat.nth Nat.Prime n := 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 $n$ , the entry at index $n$ of row $1$ of the Gilbreath triangle equals the difference of the $(n+1)$ -st and the $n$ -th prime:

d^1(n) = p_{n+1} - p_n .

Row $0$ is $n \mapsto p_n$ , the increasing enumeration of the primes from $p_0 = 2$ , and row $1$ is by definition $d^1(n) = |p_{n+1} - p_n|$ with the difference formed in the integers. The right-hand side of the asserted identity is instead a subtraction of natural numbers, which is truncated at $0$ : were $p_{n+1}$ smaller than $p_n$ for some $n$ , the right-hand side would be $0$ while the left-hand side would be positive. The claim is stated for all $n$ without hypotheses, including $n = 0$ , where it reads $d^1(0) = p_1 - p_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

Row 111 is the sequence of prime gaps

Row $1$ is the sequence of prime gaps