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

Proved

odd_sum_le_151_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 $151$ 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 151, \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 $151$ .

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_151_primes (n : ℕ) (hodd : Odd n) (hn : 1 < n) :
    ∃ s : Multiset ℕ, s.card ≤ 151 ∧ (∀ 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/75; Mann's theorem then gives K = 151. 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_151_primes. Let $n$ be a natural number (so $n \in \{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 say exactly that $n$ is an odd natural number with $n \ge 3$ . They can be satisfied, for example by $n = 3$ .

The conclusion is that there is a finite multiset $s$ of natural numbers $p_1, \dots, p_m$ (order does not matter, and the same value may occur more than once) such that:

the number of elements of $s$ , counted with multiplicity, is at most $151$ : $m \le 151$ ;
every element of $s$ is a prime number in the usual sense, meaning a natural number $p \ge 2$ whose only divisors are $1$ and $p$ . The prime $2$ is allowed;
the elements of $s$ , counted with multiplicity, add up to $n$ :

p_1 + p_2 + \cdots + p_m = n .

In other words, every odd natural number $n \ge 3$ can be written as a sum of at most $151$ primes, where primes may repeat. Nothing requires the primes to be distinct or odd, and nothing fixes the number of summands beyond the upper bound $m \le 151$ . A single summand ( $m = 1$ ) is allowed, for example when $n$ is itself prime. The empty multiset ( $m = 0$ , with sum $0$ ) can never be a witness, because $n \ge 3$ . The statement says nothing about even $n$ or about $n = 1$ .

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