Prove2Me

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

Proved
WeakGoldbach.prime_in_4e18_window_4e18_to_1e26

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

goldbachnumber-theoryprimes

For every natural number xx with

4⋅1018≤x≤1026,4\cdot 10^{18} \le x \le 10^{26},

there exists a prime pp with x<p<x+4⋅1018x < p < x + 4\cdot 10^{18}.

This middle segment of the window-covering claim follows from verified short-interval prime gaps: a prime p≤yp \le y with y−p≤y/(2.8⋅107)y - p \le y / (2.8\cdot 10^{7}) exists for every y≥1.1⋅1010y \ge 1.1\cdot 10^{10}, and applied at y=x+4⋅1018−1y = x + 4\cdot 10^{18} - 1 that bound lands inside (x,x+4⋅1018)(x, x + 4\cdot 10^{18}) whenever x≤1026x \le 10^{26}.

Formalization Note The corresponding claim is TaoFivePrimes.prime_in_short_interval.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

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

end WeakGoldbach
Source
Short-interval prime gap verification used in the five-primes work (Tao); cf. Helfgott–Platt arXiv:1305.3062v2 §4 for the complementary ladder computation

View graph