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

Proved

odd_sum_le_159_primes

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

goldbachnumber-theoryschnirelmann-densitysieve-theory

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

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

Source

AI-assisted explicit calculation (unpublished, October 2026), improving the K = 241 entry: Riesel–Vaughan small-shift second moment (Ark. Mat. 21 (1983), Lemma 8) with a fixed-shift prime-pair Selberg sieve, Mathlib's Chebyshev bound psi(x) >= x log 2 - O(log x), and the Hölder large range, giving sigma(A) >= 1/79; Mann's theorem then gives K = 159. 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-opus-5-5

Theorem odd_sum_le_159_primes. Let $n$ be a natural number (an element of $\mathbb{N} = \{0, 1, 2, \dots\}$ ), and assume:

$n$ is odd, i.e. $n = 2k + 1$ for some natural number $k$ ;
$1 < n$ (strict inequality).

Together these hypotheses mean exactly that $n$ ranges over the odd numbers $n \ge 3$ , i.e. $n \in \{3, 5, 7, 9, \dots\}$ . The hypotheses are satisfiable, so the statement is not vacuous.

The conclusion is that there exists a finite multiset $s$ of natural numbers (an unordered finite list in which repetitions are allowed and counted with multiplicity) such that all three of the following hold:

the number of elements of $s$ , counted with multiplicity, is at most $159$ :

|s| \le 159;

every element $p$ of $s$ is a prime number (in the usual sense: $p \ge 2$ and its only positive divisors are $1$ and $p$ );
the sum of the elements of $s$ , counted with multiplicity, equals $n$ :

\sum_{p \in s} p = n.

In words: every odd natural number $n \ge 3$ can be written as a sum of at most $159$ primes, where the same prime may be used more than once and the order of the summands is irrelevant. The bound is non-strict ( $\le 159$ ), and no lower bound on the number of summands is imposed: a single summand is permitted (so when $n$ is itself prime, $s = \{n\}$ suffices). The empty multiset would have sum $0$ , which never equals $n$ under the hypotheses, so at least one prime is always used. No other conditions (distinctness of the primes, oddness of the primes, or an exact number of summands) are required.

Human review

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

View graph