All-odd ternary Goldbach for $10^{27} \le n < e^{3100}$

Open

WeakGoldbach.three_odd_primes_10pow27_to_exp3100

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

goldbachnumber-theoryprimes

For every odd natural number $n$ with

10^{27} \le n < e^{3100},

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

This is the effective circle-method regime of the ternary Goldbach theorem: Helfgott's explicit major- and minor-arc bounds on the smoothed prime exponential sum prove a positive representation count for every odd $n$ in this range, and a positive count forces an all-odd triple (the $\{2,2,n-4\}$ representations contribute negligibly).

Preamble

import Mathlib

Formal statement

namespace WeakGoldbach

theorem three_odd_primes_10pow27_to_exp3100 (n : ℕ)
    (hlo : 10 ^ 27 ≤ n) (hhi : (n : ℝ) < Real.exp 3100) (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 (effective range)

View graph

All-odd ternary Goldbach for 1027≤n<e310010^{27} \le n < e^{3100}1027≤n<e3100

All-odd ternary Goldbach for $10^{27} \le n < e^{3100}$