Prove2Me

Prime gaps below 8.875×10308.875\times 10^{30} are smaller than 4⋅10184\cdot 10^{18}

Open
WeakGoldbach.prime_in_4e18_window_to_8875e30

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

goldbachnumber-theoryprimes

Put

B=4⋅1018,T=8,875,694,145,621,773,516,800,000,000,000.B = 4\cdot 10^{18}, \qquad T = 8{,}875{,}694{,}145{,}621{,}773{,}516{,}800{,}000{,}000{,}000.

For every natural number x≤T−Bx \le T - B there exists a prime pp with

x<p<x+B.x < p < x + B.

Equivalently, consecutive primes are less than BB apart throughout the range below TT. This is the covering property certified by the Helfgott–Platt computation: their prime ladder places a certified prime rung inside every consecutive window of width BB, reached interval by interval over the 492,700 blocks of width 254⋅1092^{54}\cdot 10^{9} partitioning [0,T][0, T].

Formalization Note The bound x≤T−Bx \le T - B suffices for the ladder construction (a rung is only extended while it is below T−BT - B).

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem prime_in_4e18_window_to_8875e30 (x : ℕ)
    (hx : x ≤ 8875694145621773516800000000000 - 4 * 10 ^ 18) :
    ∃ p : ℕ, x < p ∧ p < x + 4 * 10 ^ 18 ∧ Nat.Prime p := 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–§4: consecutive rungs of the prime ladder are at most Δ = 4·10^18 apart, which is precisely the statement that every window (x, x+Δ) below T contains a prime

View graph