Motivation

An additive question about the primes asks how many of them are needed to represent every integer. Shnirelman's constant is the least $k$ such that every natural number greater than $1$ is a sum of at most $k$ primes; that such a $k$ exists at all is Shnirelman's theorem (1930). The even Goldbach conjecture would give $k = 3$, and is close to equivalent to that claim, but Goldbach is open, so every bound on $k$ has come from the circle method together with explicit numerical input.

The history is a sequence of shrinking bounds, each one effective and each one resting on a numerical verification available at the time:

• 1937. Vinogradov proves that every sufficiently large odd integer is a sum of three primes, with no effective threshold (Vinogradov's theorem).
• 1956. Borozdkin makes the threshold effective; later work reduces it, and Liu and Wang bring it to $\exp(3100)$ (Liu–Wang, 2002).
• 1995. Ramaré proves that every even natural number is a sum of at most six primes, giving Shnirelman's constant $k \le 7$ (Ramaré).
• 1995. Kaniecki obtains "at most five primes" under the Riemann hypothesis (Kaniecki).
• 2012. Tao removes the hypothesis: every odd number greater than $1$ is a sum of at most five primes, unconditionally, lowering Shnirelman's constant to $k \le 6$ (arXiv:1201.6656). This mission's goal.
• 2013. Helfgott proves the ternary Goldbach conjecture outright — every odd $n > 5$ is a sum of three primes — which supersedes the statement above (arXiv:1312.7748). Neither result is formalized.

Setting

For a real number $\theta$ write $e(\theta) = \exp(2\pi i\theta)$. The von Mangoldt function $\Lambda(n)$ equals $\log p$ when $n = p^m$ is a prime power and $0$ otherwise; it is Mathlib's ArithmeticFunction.vonMangoldt.

The paper does not work with the sharp-cutoff exponential sum $S(x,\alpha) = \sum_{n \le x} \Lambda(n)e(\alpha n)$ but with a smoothed variant. For a piecewise smooth $\eta : \mathbb{R} \to \mathbb{C}$ and a modulus $q_0$, set

$$S_{\eta,q_0}(x,\alpha) \;:=\; \sum_{n} \Lambda(n)\,e(\alpha n)\, \mathbf{1}_{(n,q_0)=1}\,\eta(n/x).$$

The modulus $q_0$ is a technical device: taking $q_0 = 2$ restricts the sum to odd $n$ and saves a factor of two in the explicit constants. Because of that restriction it is $4\alpha$, not $\alpha$, that gets approximated by a rational $a/q$.

Two explicit cutoffs are fixed. The Lipschitz cutoff

$$\eta_0(t) := 4\big(\log 2 - |\log 2t|\big)_+$$

has unit mass and is supported on $[1/4, 1]$; it is chosen because it factorises the Type II sums. The $L^2$-normalised cutoff

$$\eta_1(t) := \big(1 - 10\,\mathrm{dist}(t,[0.2,0.8])\big)_+$$

is supported on $[0.1,0.9]$ and symmetric, $\eta_1(1-t) = \eta_1(t)$.

Throughout, $O^*(Y)$ denotes a quantity of magnitude at most $Y$ — an explicit bound, not an asymptotic one. Two numerical constants are fixed once and for all: $T_0 := 3.29\times 10^9$ and $N_0 := 4\times 10^{14}$.

Formalization targets

Goal (Theorem 1.4)

$$\forall n \text{ odd},\ n > 1 \;\Longrightarrow\; \exists\, p_1,\dots,p_k \text{ prime},\ k \le 5,\ n = p_1 + \cdots + p_k.$$

The goal fixes no constants and no thresholds, so no later improvement can invalidate it.

The milestone list is the paper's own attack path, in its numbering: the two numerical verifications (Theorems 1.5, 1.6) and the short-interval prime bound (Theorem 8.1) that together settle $n \le 8.7\times10^{36}$; the $L^2$ apparatus (Lemma 4.4, Proposition 4.10) and Vaughan-type identity (Lemma 4.11) feeding the minor-arc bound (Theorem 5.1) and hence the main exponential sum estimate (Theorem 1.3); the major-arc analysis (Proposition 7.2); and the circle-method core (Theorem 8.2).

Significance

The result itself. Theorem 1.4 lowers Shnirelman's constant from $7$ to $6$ and removes the Riemann hypothesis from Kaniecki's conditional "five primes". Its durable content, however, is not the headline but the explicit exponential sum estimate of Theorem 1.3: a bound on $|S_{\eta_0,q_0}(x,\alpha)|$ with constants small enough to be useful for $x$ between $10^{30}$ and $10^{1300}$, a range where the asymptotically superior estimates of Vinogradov, Chen–Daboussi and Ramaré carry constants too large or too ineffective to apply. That estimate is the reusable object; it has been improved since (Helfgott–Platt) but not superseded in method.

Formalizing it. Status honesty matters here. Theorem 1.4 is closed mathematics, and as a statement it was superseded within a year by Helfgott's ternary Goldbach theorem, which gives three primes for every odd $n > 5$ and hence five a fortiori. Neither Tao's theorem nor Helfgott's is formalized anywhere, and this mission does not claim to be attacking an open problem: the work is formalizing a known, fully explicit proof. That proof happens to be an unusually good formalization target, because every constant in it is written down.

The platform already hosts the surrounding infrastructure. The CircleMethod namespace carries a large verified development of Hardy–Littlewood apparatus following Vaughan, and the ThreePrimes namespace carries a machine-checked proof of Vinogradov's three primes theorem conditional on Siegel–Walfisz. This mission sits directly downstream of both and should import from them rather than rebuild.

Difficulty

The obvious route — deduce five primes from three primes — fails on the range where it is needed. Vinogradov's theorem is asymptotic, and the best effective threshold is $\exp(3100)$; below it the theorem says nothing, and $\exp(3100)$ is far beyond any possible exhaustive check. So the entire difficulty lives in the window $8.7\times10^{36} \le x \le \exp(3100)$, which must be handled by a circle-method argument carrying explicit constants at every step.

Within that window the specific obstruction is the minor arc $T_0/x \ll \|\alpha\|_{\mathbb{R}/\mathbb{Z}} \ll 1/N_0$. A direct Plancherel bound on the $L^2$ side costs a factor of $\log x$, which is more than the argument can afford; Montgomery's uncertainty principle cuts the loss to roughly $2\log x/\log N_0$, and only a large-sieve estimate on prime pairs brings it down to a bounded factor of $8$. On the $L^\infty$ side, Theorem 1.3 must be non-trivial across the whole window, which is why the refinements (1.10)–(1.12) for $q$ near $1$ and near $x$ exist at all. Neither bound alone suffices; the proof closes only because both are pushed to explicit constants simultaneously.

Formalization scope

The goal is stated over $\mathbb{N}$ as a Multiset ℕ of cardinality at most $5$ whose members are all Nat.Prime and whose sum is $n$. A multiset, not a list or a finset: repetition is essential ($9 = 3+3+3$) and order is not. "At most five" is not "exactly five" — $3$ is a sum of one prime and cannot be a sum of five, since the least sum of five primes is $10$. A formalization asserting exactly five primes is false, not merely weaker.

The goal admits no trivializing reading: the empty multiset has sum $0 \ne n$, and the cardinality bound is on the multiset itself, so no prime can be counted with multiplicity zero to evade it.

Everything else in the mission is stated with explicit constants and $O^*(\cdot)$ bounds rather than asymptotic notation, matching the paper: $X = O^*(Y)$ becomes $\|X\| \le Y$ outright. Sums over $n$ are unrestricted sums against a compactly supported cutoff, not sums over Finset.range. Real powers are Real.rpow. The two cutoffs $\eta_0,\eta_1$ and the sum $S_{\eta,q_0}$ are published as mission definitions; solvers should use them verbatim rather than re-deriving equivalent forms.

Three of the milestones are honest dead weight for a solver to attempt directly, and are listed so the dependency graph is truthful rather than because they are tractable. Theorem 1.5 (all zeroes of $\zeta$ up to height $3.29\times10^9$ lie on the critical line) and Theorem 1.6 (every even number up to $4\times10^{14}$ is a sum of two primes) are finite, decidable statements that Lean can express and that are true, but each represents a verified computation of a scale no current proof assistant can replay — Theorem 1.6 alone is $2\times10^{14}$ cases. Theorem 8.1 is quoted from Ramaré–Saouter and itself depends on Theorem 1.5. They are leaves that will stay open; a solver's effort is far better spent on the analytic milestones, and the circle-method core (Theorem 8.2) can be closed independently of them.

A complete development additionally needs the smoothed Vaughan identity bookkeeping, the large sieve in Siebert's form, the von Mangoldt explicit formula with a zero sum (Proposition 7.1), and Bourgain's trick of taking one of the three summands of size $x/K$. The exponential sum machinery is reusable well beyond this mission — it is the standard input to every explicit Goldbach-type result. Contributions to any milestone are welcome independently, and a formalization of Helfgott's theorem that closes the goal by a different route would be an entirely acceptable solution.

Selected references

• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Mathematics of Computation 83 (2014), 997–1038. arXiv:1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. arXiv:1312.7748
• H. A. Helfgott and D. Platt, Numerical verification of the ternary Goldbach conjecture up to $8.875\cdot10^{30}$, 2013. arXiv:1305.3062
• O. Ramaré, On Shnirel'man's constant, Ann. Scuola Norm. Sup. Pisa 22 (1995), 645–706. numdam
• L. Kaniecki, On Shnirelman's constant under the Riemann hypothesis, Acta Arithmetica 72 (1995), 361–374. doi:10.4064/aa-72-4-361-374
• J. Richstein, Verifying the Goldbach conjecture up to $4\cdot10^{14}$, Mathematics of Computation 70 (2001), 1745–1749. doi:10.1090/S0025-5718-00-01290-4
• O. Ramaré and Y. Saouter, Short effective intervals containing primes, Journal of Number Theory 98 (2003), 10–33. doi:10.1016/S0022-314X(02)00029-X
• M. C. Liu and T. Z. Wang, On the Vinogradov bound in the three primes Goldbach conjecture, Acta Arithmetica 105 (2002), 133–175. doi:10.4064/aa105-2-3
• H. L. Montgomery, The analytic principle of the large sieve, Bulletin of the AMS 84 (1978), 547–567. doi:10.1090/S0002-9904-1978-14497-8
• R. C. Vaughan, The Hardy–Littlewood Method, 2nd ed., Cambridge University Press, 1997. doi:10.1017/CBO9780511470929