Every Odd Number Greater Than1 is the Sum of at Most19 Primes
ProvedOddGoldbach19.odd_sum_le_19_primesEvery odd number greater than 1 is the sum of at most 19 primes, collected as a multiset (repetition allowed, order irrelevant).
Preamble
import Mathlib
Formal statement
theorem OddGoldbach19.odd_sum_le_19_primes (n : ℕ) (hodd : Odd n) (hn : 1 < n) :
∃ s : Multiset ℕ, s.card ≤ 19 ∧ (∀ p ∈ s, Nat.Prime p) ∧ s.sum = n := by
sorry
Source
Known odd-integer corollary of the19-prime bound of H.Riesel and R.C.Vaughan, On sums of primes, Arkiv for Matematik21(1983), pp45-74, https://doi.org/10.1007/BF02384300 . This formal proof uses the finite-shift second moment and Schnirelmann-density method, with its own explicitly proved thresholds and kernel-checked finite arithmetic.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.