A prime in $(x,\, x+4\cdot 10^{18})$ for every $x \le 4\cdot 10^{18}$

Proved

WeakGoldbach.prime_in_4e18_window_below_4e18

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

goldbachnumber-theoryprimes

For every natural number $x \le 4\cdot 10^{18}$ there exists a prime $p$ with

x < p < x + 4\cdot 10^{18}.

This is the elementary base of the window-covering statement used to build the Helfgott–Platt prime ladder. For $x \ge 1$ it follows from Bertrand's postulate, which provides a prime $p$ with $x < p \le 2x$ , and $2x \le x + 4\cdot 10^{18}$ when $x \le 4\cdot 10^{18}$ ; the case $x = 0$ is witnessed by $p = 3$ .

Formalization Note Mathlib supplies Bertrand's postulate as Nat.exists_prime_lt_and_le_two_mul.

Preamble

import Mathlib

Formal statement

namespace WeakGoldbach

theorem prime_in_4e18_window_below_4e18 (x : ℕ) (hx : x ≤ 4 * 10 ^ 18) :
    ∃ p : ℕ, x < p ∧ p < x + 4 * 10 ^ 18 ∧ Nat.Prime p := by
  sorry

end WeakGoldbach

Source

Bertrand's postulate; this is the provable base segment of the covering claim certified computationally by Helfgott–Platt, arXiv:1305.3062v2 §4

View graph

A prime in (x, x+4⋅1018)(x,\, x+4\cdot 10^{18})(x,x+4⋅1018) for every x≤4⋅1018x \le 4\cdot 10^{18}x≤4⋅1018

A prime in $(x,\, x+4\cdot 10^{18})$ for every $x \le 4\cdot 10^{18}$