Prove2Me

Prime ladder step: a prime in [n−4⋅1018−2, n−4][n-4\cdot 10^{18}-2,\, n-4] for each odd n≤8.875×1030n \le 8.875\times 10^{30}

Open
WeakGoldbach.prime_in_window_4e18_add_two

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

goldbachnumber-theoryprimes

This is the covering property certified by the Helfgott–Platt prime ladder computation.

For every odd natural number nn with

4⋅1018+5≤n≤8,875,694,145,621,773,516,800,000,000,000=:T,4\cdot 10^{18} + 5 \le n \le 8{,}875{,}694{,}145{,}621{,}773{,}516{,}800{,}000{,}000{,}000 =: T,

there exists a prime pp with

4≤n−p≤4⋅1018+2,4 \le n - p \le 4\cdot 10^{18} + 2,

i.e. the interval [n−4⋅1018−2, n−4][n - 4\cdot 10^{18} - 2,\, n - 4] contains a prime.

Helfgott and Platt computed an explicit ladder of primes r0<r1<…r_0 < r_1 < \dots reaching past TT, each consecutive rung at most Δ=4⋅1018\Delta = 4\cdot 10^{18} apart (rungs are Proth primes k⋅252+1k\cdot 2^{52} + 1 where available, certified by Proth's theorem, and general primes otherwise). Taking pp to be the largest rung at most n−4n - 4, the next rung satisfies rj+1≥n−2r_{j+1} \ge n - 2 (since n−3n - 3 is even and exceeds 22), whence

n−p=(n−rj+1)+(rj+1−rj)≤2+Δ.n - p = (n - r_{j+1}) + (r_{j+1} - r_j) \le 2 + \Delta.

Formalization Note The distance is stated on Nat truncated subtraction; since 4≤n−p4 \le n - p it agrees with the integer difference.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem prime_in_window_4e18_add_two (n : ℕ) (hodd : Odd n)
    (hlo : 4 * 10 ^ 18 + 5 ≤ n) (hhi : n ≤ 8875694145621773516800000000000) :
    ∃ p : ℕ, Nat.Prime p ∧ 4 ≤ n - p ∧ n - p ≤ 4 * 10 ^ 18 + 2 := by
  sorry

end WeakGoldbach
Source
H. A. Helfgott and D. J. Platt, Numerical verification of the ternary Goldbach conjecture up to 8.875e30, arXiv:1305.3062v2, §3 (the prime ladder algorithm, rung gap Δ = 4·10^18) and §4 (implementation over 492,700 intervals of width 2^54·10^9 reaching T), https://arxiv.org/abs/1305.3062

View graph