Prove2Me

Verified binary Goldbach range (4⋅1014, 4⋅1018](4\cdot 10^{14},\, 4\cdot 10^{18}]

Open
WeakGoldbach.verified_two_primes_4e14_to_4e18

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

goldbachnumber-theoryprimes

For every even natural number mm with

4⋅1014<m≤4⋅1018,4\cdot 10^{14} < m \le 4\cdot 10^{18},

there exist primes pp and qq with m=p+qm = p + q.

This is the extension segment of the verified binary Goldbach range: Richstein's computation reaches 4⋅10144\cdot 10^{14}, and Oliveira e Silva–Herzog–Pardi extend it to 4⋅10184\cdot 10^{18}. Together with Richstein2001.even_goldbach_up_to_4e14 it gives the full verified range through 4⋅10184\cdot 10^{18}.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem verified_two_primes_4e14_to_4e18 (m : ℕ) (hlo : 4 * 10 ^ 14 < m)
    (hB : m ≤ 4 * 10 ^ 18) (he : Even m) :
    ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ m = p + q := by
  sorry

end WeakGoldbach
Source
T. Oliveira e Silva, S. Herzog, and S. Pardi, Empirical verification of the even Goldbach conjecture and computation of prime gaps up to 4·10^18, Math. Comp. 83 (2014), no. 288, 2033–2060 (the segment above Richstein's 4·10^14)

View graph