Every Odd Number Greater Than 1 is the Sum of at Most 973 Primes
Provedodd_sum_le_973_primesEvery odd natural number greater than is a sum of at most primes, with repetition allowed.
Precisely: for every with odd and there is a finite multiset of natural numbers such that
Here counts elements with multiplicity, so the same prime may be used several times, and the order of the summands is irrelevant.
This is the campaign statement of Odd numbers as sums of primes with the value .
Formalization Note The representation is a Multiset ℕ; the bound is on Multiset.card, so repeated primes count separately.
import Mathlib
theorem odd_sum_le_973_primes (n : ℕ) (hodd : Odd n) (hn : 1 < n) :
∃ s : Multiset ℕ, s.card ≤ 973 ∧ (∀ p ∈ s, Nat.Prime p) ∧ s.sum = n := by
sorry
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Read-back of odd_sum_le_973_primes. Let be any natural number with two hypotheses:
- is odd, meaning for some ;
- , which is strict.
Together these say that is an odd number with . Both hypotheses can be satisfied, for example by . The cases and are excluded, and so are all even .
The statement says that for every such there exists a finite multiset of natural numbers satisfying all three of these conditions:
Here are the terms and edge cases:
- A multiset is an unordered finite collection in which an element may appear more than once.
- is the number of elements of counted with multiplicity. The bound is "at most 973" (), not "exactly 973".
- The sum also counts each element with its multiplicity.
- "Prime" is the usual notion for natural numbers: and the only divisors of are and .
So the conclusion says that can be written as a sum of at most primes, where repeats are allowed and order does not matter. Nothing requires the primes to be distinct, to be odd, or to be different from . Nothing requires the number of summands to be any particular value other than being at most ; a single summand ( when is prime) is allowed. The empty multiset has sum , so it can never be a witness, because . The statement only asserts that such an exists. It says nothing about being unique or how to construct it.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.