Prove2Me

Verified all-odd ternary Goldbach range [9, 8.875×1030][9,\, 8.875\times 10^{30}]

Open
WeakGoldbach.verified_three_odd_primes_to_8875e30

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

goldbachnumber-theoryprimes

For every odd natural number nn with

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

there exist odd primes p,q,rp, q, r with n=p+q+rn = p + q + r.

This is the all-odd strengthening of the verified ternary range: writing n=3+(n−3)n = 3 + (n-3) requires an odd-prime partition of the even number n−3n - 3 — confirmed throughout the range by the partition data of Oliveira e Silva–Herzog–Pardi.

Preamble
import Mathlib
Formal statement
namespace WeakGoldbach

theorem verified_three_odd_primes_to_8875e30 (n : ℕ)
    (hlo : 9 ≤ n) (hhi : n ≤ 8875694145621773516800000000000) (hodd : Odd n) :
    ∃ p q r : ℕ,
      Nat.Prime p ∧ Nat.Prime q ∧ Nat.Prime r ∧
      Odd p ∧ Odd q ∧ Odd r ∧ n = p + q + r := by
  sorry

end WeakGoldbach
Source
Helfgott–Platt, arXiv:1305.3062v2 (verified range), combined with the odd-prime-partition fact implicit in the OeS–Herzog–Pardi binary data, doi:10.1090/s0025-5718-2013-02787-1

View graph