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

Proved

odd_sum_le_85_primes

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

goldbachnumber-theoryschnirelmann-densitysieve-theory

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

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

Source

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

Plain-language reading

For every natural number n that is odd and greater than 1, there is a multiset s of natural numbers such that:

s has at most 85 elements (counted with multiplicity),
every element of s is prime,
the elements of s sum to n.

In words: every odd integer n > 1 is a sum of at most 85 primes. Repetition is allowed because s is a multiset.

Observations

Types: n : ℕ, so no negative or real edge cases. Odd n with 1 < n excludes only n = 1 (and 0 is even).
The statement is not vacuous. Small cases: n = 3, 5, 7 are prime (card 1), and 9 = 2+7. By Helfgott's ternary Goldbach theorem every odd n ≥ 7 is a sum of 3 primes, so the statement is true, with a bound (85) far weaker than needed. Without that theorem it is a Schnirelmann-type claim.
The empty multiset has sum 0, so it cannot satisfy sum = n for n > 1. The card bound cannot be met trivially.
Proof body is sorry, so nothing is established. The statement is well-formed and uses only Nat.Prime and Multiset.sum.
Nothing hidden: no extra hypotheses, no unusual coercions, no definitions beyond Mathlib.

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