Ternary Goldbach with odd primes for $n \ge 10^{27}$

Open

WeakGoldbach.three_odd_primes_ge_10pow27

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

goldbachnumber-theoryprimes

For every odd natural number $n \ge 10^{27}$ there exist odd primes $p, q, r$ with $n = p + q + r$ .

This is the analytic half of the ternary Goldbach theorem: Helfgott's circle-method argument proves every odd $n \ge 10^{27}$ is a sum of three odd primes.

Preamble

import Mathlib

Formal statement

namespace WeakGoldbach

theorem three_odd_primes_ge_10pow27 (n : ℕ)
    (hn : 10 ^ 27 ≤ n) (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

H. A. Helfgott, The ternary Goldbach conjecture is true, arXiv:1312.7748

View graph

Ternary Goldbach with odd primes for n≥1027n \ge 10^{27}n≥1027

Ternary Goldbach with odd primes for $n \ge 10^{27}$