Every odd number greater than 1 is the sum of at most 23 primes
ProvedOAI.OddGoldbach.odd_sum_le_23_primesnumber-theory
Every odd natural number greater than 1 can be written as a sum of at most 23 primes. Repetition is allowed and order is irrelevant; the summands form a multiset. This is the Odd Goldbach campaign statement with bound 23.
Preamble
import Mathlib
Formal statement
theorem OAI.OddGoldbach.odd_sum_le_23_primes (n : ℕ) (hodd : Odd n) (hn : 1 < n) :
∃ s : Multiset ℕ, s.card ≤ 23 ∧ (∀ p ∈ s, Nat.Prime p) ∧ s.sum = n := by
sorry
Source
Numerical refinement of the accepted 25-prime Schnirelmann–Mann formalization https://prove2.me/theorems/ba75c64f-9452-4582-83b3-77b31da8e4dc . It uses a newly certified 1000-prime finite sieve set and the existing Riesel–Vaughan interval inputs; the shared definitions and quantified campaign goal are unchanged. This is a formalized constant improvement of the existing method, not a new proof of weak Goldbach.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.