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

Proved

odd_sum_le_27_primes

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

Every odd natural number greater than $1$ is a sum of at most $27$ 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 27, \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 $27$ .

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_27_primes (n : ℕ) (hodd : Odd n) (hn : 1 < n) :
    ∃ s : Multiset ℕ, s.card ≤ 27 ∧ (∀ p ∈ s, Nat.Prime p) ∧ s.sum = n := by
  sorry

Source

AI-assisted explicit calculation (unpublished, October 2026), improving the K = 41 entry: Riesel-Vaughan's singular-series-weighted large range (Ark. Mat. 21 (1983), Sec. 8) with Dirichlet characters and the platform's weighted large sieve (MVSieve nodes), the Riesel-Vaughan small-shift range (Lemma 8) with Siebert's prime-pair bound (TaoFivePrimes.siebert_prime_pair_bound), and Chebyshev's psi(x) >= 0.9212x - 5 log x + 5 in place of Rosser-Schoenfeld, giving sigma(A) >= 1/13; Mann's theorem then gives K = 27. Framework: P. Pollack, Not Always Buried Deep, Ch. 6 Sec. 6, https://www.pollack-math.net/NABDofficial.pdf

Read-back

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

The statement is a theorem named odd_sum_le_27_primes. It takes two hypotheses about a natural number $n$ and concludes that a certain multiset of primes exists.

Variables and hypotheses. Let $n$ be a natural number, so $n \in \mathbb{N} = \{0, 1, 2, \dots\}$ .

Hypothesis hodd: $n$ is odd, meaning $n = 2k+1$ for some natural number $k$ .
Hypothesis hn: $1 < n$ .

Together these say $n$ is an odd natural number with $n \ge 3$ . Both hypotheses can be satisfied, for example by $n = 3$ , so the theorem is not vacuous. The excluded values are $n = 0$ and $n = 1$ , and $n = 1$ is excluded explicitly by hn.

Conclusion. There exists a finite multiset $s$ of natural numbers, that is, a finite collection of natural numbers in which repetition is allowed and order is irrelevant, such that all three of the following hold:

$|s| \le 27$ . Here $|s|$ is the cardinality counted with multiplicity, so the number of elements, repeats included, is at most 27. This is a non-strict bound, so $|s| = 27$ is allowed. Nothing requires $|s|$ to be at least any particular value.
Every element $p \in s$ is a prime number, that is, $p \in \mathbb{N}$ with $p \ge 2$ whose only positive divisors are $1$ and $p$ .
$\displaystyle \sum_{p \in s} p = n$ , where the sum is taken with multiplicity, so a prime that occurs $m$ times in $s$ contributes $m \cdot p$ .

Remarks on what is and is not asserted.

The primes are not required to be distinct, because $s$ is a multiset.
The only upper bound on the size is 27. The statement does not say the number of primes is exactly 27, does not bound the size of the primes, and does not say the representation is unique.
The statement does not give any construction of $s$ . It only asserts that some such $s$ exists for each $n$ satisfying the hypotheses.
The bound 27 is a fixed constant that does not depend on $n$ . The statement therefore asserts that for every odd $n > 1$ , however large, $n$ is a sum of at most 27 primes with repetition allowed.

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