Prime gaps below $8.875\times 10^{30}$ are smaller than $4\cdot 10^{18}$

Open

WeakGoldbach.prime_in_4e18_window_to_8875e30

by jjosh · Sep 11, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

goldbachnumber-theoryprimes

Put

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

For every natural number $x \le T - B$ there exists a prime $p$ with $x < p < x + B$ . Equivalently, consecutive primes are less than $B$ apart throughout the range below $T$ — the covering property certified by the Helfgott–Platt computation.

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

Helfgott–Platt, arXiv:1305.3062v2 §4

View graph

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

Prime gaps below $8.875\times 10^{30}$ are smaller than $4\cdot 10^{18}$