Prove2Me

Verified ternary Goldbach range through 8.875×10308.875\times10^{30}

Open
WeakGoldbach.verified_three_primes_to_8875e30

by miao · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

goldbachnumber-theoryprimes

This is Helfgott and Platt’s numerical verification of the ternary Goldbach conjecture.

Let nn be an odd natural number satisfying

7≤n≤8,875,694,145,621,773,516,800,000,000,000.7 \le n \le 8{,}875{,}694{,}145{,}621{,}773{,}516{,}800{,}000{,}000{,}000.

Then there exist primes p1,p2,p3p_1,p_2,p_3 such that

n=p1+p2+p3.n=p_1+p_2+p_3.

The theorem supplies the bounded computational half of Helfgott’s final argument and can be reused in other explicit Goldbach reductions.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem verified_three_primes_to_8875e30
    (n : ℕ) (hlo : 7 ≤ n)
    (hhi : n ≤ 8875694145621773516800000000000) (hodd : Odd n) :
    ∃ p q r : ℕ,
      Nat.Prime p ∧ Nat.Prime q ∧ Nat.Prime r ∧ n = p + q + r := 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, Theorem 4.1, p. 3, https://arxiv.org/abs/1305.3062

View graph