Every Odd Number Greater Than 1 is the Sum of at Most 41 Primes

Proved

odd_sum_le_41_primes

by xuanji · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

goldbachnumber-theoryschnirelmann-densitysieve-theory

Every odd natural number greater than $1$ is a sum of at most $41$ primes, with repetition allowed.

Precisely: for every $n \in \mathbb{N}$ with $n$ odd and $n > 1$ there is a finite multiset $s$ of natural numbers such that

|s| \le 41, \qquad \text{every } p \in s \text{ is prime}, \qquad \sum_{p \in s} p = n.

Here $|s|$ 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 $41$ .

Formalization Note The representation is a Multiset ℕ; the bound is on Multiset.card, so repeated primes count separately.

Preamble

import Mathlib

Formal statement

theorem odd_sum_le_41_primes (n : ℕ) (hodd : Odd n) (hn : 1 < n) :
    ∃ s : Multiset ℕ, s.card ≤ 41 ∧ (∀ p ∈ s, Nat.Prime p) ∧ s.sum = n := by
  sorry

Source

AI-assisted explicit calculation (unpublished, October 2026), improving the K = 85 entry: the sharp singular-series weight K(s) = prod_{p | s, p > 2} (p-1)/(p-2) via the platform's proved Siebert prime-pair bound (TaoFivePrimes.siebert_prime_pair_bound) in the Riesel–Vaughan small-shift range (Ark. Mat. 21 (1983), Lemma 8), a Goldbach analogue of Siebert's bound from the platform's PrimePairSieve nodes in the large range, the twelfth moment of K(s) and Hölder, giving sigma(A) >= 1/20; Mann's theorem then gives K = 41. Framework: P. Pollack, Not Always Buried Deep, Ch. 6 §6, https://www.pollack-math.net/NABDofficial.pdf

Read-back

What the Lean code literally says, in plain math · claude-sonnet-5-5

Read-back. The declaration is a theorem named odd_sum_le_41_primes. It takes a natural number $n \in \mathbb{N}$ (so $n \ge 0$ ), together with two hypotheses: $n$ is odd, i.e. $n = 2k+1$ for some natural number $k$ , and $1 < n$ . Since $n$ is odd, the second hypothesis only excludes $n = 1$ ; $n = 0$ is already ruled out by oddness.

The conclusion is that there exists a finite multiset $s$ of natural numbers (repetitions allowed, order irrelevant) satisfying all three of the following:

|s| \le 41, \qquad \forall p \in s,\ p \text{ is prime}, \qquad \sum_{p \in s} p = n,

where $|s|$ is the cardinality of $s$ counted with multiplicity, "prime" is the standard notion (a natural number $p \ge 2$ whose only divisors are $1$ and $p$ ), and the sum is taken with multiplicity.

Remarks on what the statement literally includes. The bound is "at most 41" (non-strict), counting repeated primes separately. The primes need not be distinct, and they need not be odd, so $2$ may appear any number of times. The multiset is only required to exist for each such $n$ . The multiset $s$ may depend on $n$ , and no bound on $n$ is imposed. Nothing is claimed about uniqueness, about the specific primes used, or about any smaller bound than 41. The statement is not vacuous: its hypotheses are satisfiable (e.g. $n = 3, 5, 7, \dots$ ).

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by xuanji · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph