Helfgott–Platt prime-ladder certificate through $8.875\times10^{30}$

Open

WeakGoldbach.prime_ladder_to_8875e30

by con · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

computational-number-theorygoldbachnumber-theory

Put

B=4\cdot10^{18},\qquad T=8875694145621773516800000000000.

There is a finite increasing sequence of odd primes

p_0,p_1,\ldots,p_k

with endpoint and spacing bounds

p_0\le B,\qquad T\le p_k+B,\qquad p_i<p_{i+1}<p_i+B\quad(0\le i<k).

This isolates the prime-ladder certificate underlying the bounded ternary Goldbach verification of Helfgott and Platt. It contains only primality, parity, ordering, spacing, and endpoint assertions; it assumes no binary or ternary Goldbach theorem.

Formalization Note. The sequence is represented by a function on the natural numbers, with conditions only on indices through $k$ . Later values are immaterial. The strict upper gap follows the strict search window in Section 3 of the source; because the primes are odd and $B$ is even, it gives gaps at most $B-2$ . This margin is needed to leave an even remainder of at least four. This is a certificate-level formulation of the computation described in Sections 3–4, not a separately numbered theorem in the paper. No certificate data or formal verification of the computation is supplied by this open statement.

Preamble

import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Algebra.Ring.Parity

Formal statement

theorem WeakGoldbach.prime_ladder_to_8875e30 :
    ∃ (k : ℕ) (p : ℕ → ℕ),
      (∀ i, i ≤ k → Nat.Prime (p i) ∧ Odd (p i)) ∧
      p 0 ≤ 4 * 10 ^ 18 ∧
      (∀ i, i < k → p i < p (i + 1) ∧ p (i + 1) < p i + 4 * 10 ^ 18) ∧
      8875694145621773516800000000000 ≤ p k + 4 * 10 ^ 18 := by sorry

Source

H. A. Helfgott and D. J. Platt, Numerical Verification of the Ternary Goldbach Conjecture up to 8.875e30, arXiv:1305.3062v2, Section 3 (p. 2), algorithm steps 2-4 (strict search bound N0+Delta), and Section 4 (p. 3), ladder endpoint/spacing checks and Theorem 4.1: https://arxiv.org/abs/1305.3062

View graph

Helfgott–Platt prime-ladder certificate through 8.875×10308.875\times10^{30}8.875×1030

Helfgott–Platt prime-ladder certificate through $8.875\times10^{30}$