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

Proved

odd_sum_le_6101_primes

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

goldbachnumber-theoryschnirelmann-densitysieve-theory

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

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

Source

AI-assisted explicit calculation (unpublished, October 2026): weighted second-moment / Cauchy–Schwarz argument, sigma(A) >= 1/2200, m = 1525, K = 4m + 1 = 6101; framework: P. Pollack, Not Always Buried Deep, Ch. 6 §6, pp. 196–201, https://www.pollack-math.net/NABDofficial.pdf

Read-back

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

For every natural number $n$ that is odd and satisfies $1 < n$ (so $n \in \{3, 5, 7, 9, \dots\}$ ), the statement says that $n$ can be written as a sum of at most $6101$ primes, with repeats allowed. More precisely, it asserts that there exists a finite multiset $s$ of natural numbers satisfying all three of the following:

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

Notes on how to read each part:

Variables and hypotheses.
- $n$ is a natural number, and natural numbers here include $0$ .
- The first hypothesis is that $n$ is odd, meaning $n = 2k + 1$ for some natural number $k$ .
- The second hypothesis is the strict inequality $1 < n$ .
- Together the two hypotheses exclude $n = 1$ and every even $n$ . They are satisfiable, for example by $n = 3$ .
- There are no other hypotheses or parameters.
What $s$ is.
- $s$ is a multiset, meaning an unordered finite collection in which the same prime may appear more than once.
- $|s|$ is its cardinality counted with multiplicity. For example, $\{3, 3, 5\}$ has cardinality $3$ .
- $\sum_{p \in s} p$ is also the sum with multiplicity.
The bound.
- The bound $|s| \le 6101$ is non-strict.
- No lower bound on the number of summands is required.
- Since $n \ge 3$ , the multiset cannot be empty. So the number of summands is between $1$ and $6101$ inclusive.
"Prime" is the usual notion: a natural number $p \ge 2$ whose only divisors are $1$ and $p$ . In particular, $2$ counts as a prime, so a summand equal to $2$ is allowed.
No other restrictions. The statement asks only that some such representation exists. It does not require the primes to be distinct, odd, or ordered in any way, and it does not require the representation to be unique.

Human review

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

View graph