Every odd number greater than 1 is the sum of at most five primes

Open

TaoFivePrimes.five_primes

by Jack McCarthy · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricscircle-methodgoldbachnumber-theory

Every odd natural number $n > 1$ can be written as $n = p_1 + \cdots + p_k$ for some $k \le 5$ and primes $p_1,\dots,p_k$ , not necessarily distinct.

This is the main theorem of Tao's 2012 paper. It improves on Ramar'e's result that every even number is a sum of at most six primes, and lowers Shnirelman's constant from $7$ to $6$ . Kaniecki had obtained the same conclusion under the Riemann hypothesis; Tao's proof is unconditional, though it quotes two large numerical verifications.

The primes are collected as a multiset, so repetition is allowed ( $9 = 3+3+3$ ) and order is irrelevant. Note that at most five is essential and cannot be strengthened to exactly five: the least sum of five primes is $10$ , so $3$ , $5$ and $7$ are not sums of exactly five primes.

Preamble

import Mathlib

Formal statement

namespace TaoFivePrimes

theorem five_primes (n : ℕ) (hodd : Odd n) (hn : 1 < n) :
    ∃ s : Multiset ℕ, s.card ≤ 5 ∧ (∀ p ∈ s, Nat.Prime p) ∧ s.sum = n := by
  sorry

end TaoFivePrimes

Source

Terence Tao, Every odd number greater than 1 is the sum of at most five primes, Mathematics of Computation 83 (2014), 997-1038, https://arxiv.org/abs/1201.6656, Theorem 1.4 (p. 6)

Read-back

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

For every natural number $n$ , the statement asserts the following implication.

Hypotheses. $n$ is a natural number ( $n \in \mathbb{N}$ , so $n \ge 0$ ) satisfying two conditions:

$n$ is odd, i.e. there exists $k \in \mathbb{N}$ with $n = 2k + 1$ ;
$1 < n$ (strictly greater than $1$ ).

Together these force $n \ge 3$ and $n$ odd, so the hypotheses are jointly satisfiable (e.g. $n = 3$ ) and the statement is not vacuous.

Conclusion. There exists a finite multiset $s$ of natural numbers — an unordered finite collection in which the same number may occur several times, each occurrence counted separately — such that all three of the following hold simultaneously:

\operatorname{card}(s) \le 5, \qquad \forall\, p \in s,\ p \text{ is prime}, \qquad \sum_{p \in s} p = n .

Here $\operatorname{card}(s)$ is the number of elements of $s$ counted with multiplicity, and the bound is non-strict ( $\le 5$ , not $= 5$ and not $< 5$ ), so multisets of size $0, 1, 2, 3, 4$ or $5$ are all permitted by that clause; the empty multiset, whose sum is $0$ , is excluded only because $\sum_{p\in s} p = n > 1$ . The primality condition quantifies over every element of $s$ : each element $p$ satisfies primality in the natural numbers ( $p \ge 2$ and its only divisors are $1$ and $p$ ). The sum $\sum_{p \in s} p$ is the sum of all elements of $s$ with multiplicity, computed in $\mathbb{N}$ , and is required to be exactly $n$ .

What is not required. The elements of $s$ need not be distinct — a prime may be repeated up to five times. The primes are not required to be odd; $2$ may occur as an element. No lower bound is placed on $\operatorname{card}(s)$ , no minimality of the number of summands is claimed, and the multiset $s$ is asserted only to exist, not to be unique ( $\exists$ , not $\exists!$ ). Nothing relates $s$ to the witness $k$ from the oddness hypothesis, and no effective or constructive procedure for producing $s$ is asserted.

Human review

Endorsed by marwahaha · Sep 7, 2026
Endorsed by Jack McCarthy · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph