Liu–Wang: every odd $n \ge e^{3100}$ is a sum of three primes

Open

TaoFivePrimes.liu_wang_three_primes

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

additive-number-theorycircle-methodgoldbachnumber-theorythree-primes

Effective Vinogradov theorem (Liu–Wang). Every odd integer $n \ge e^{3100}$ is the sum of three primes,

n = p_1 + p_2 + p_3 .

This is the explicit form of Vinogradov's three primes theorem with the threshold made numerical: Vinogradov (1937) proved the statement for all sufficiently large odd $n$ with no effective bound, Borozdkin (1956) gave the first explicit threshold, and Liu and Wang (2002) lowered it to $e^{3100}$ by a careful explicit circle-method argument.

Role in Tao's proof. Tao's paper quotes this result to dispose of the range $x > e^{3100}$ : for such odd $x$ three primes already suffice. The paper's own analytic work (Theorem 8.2, the circle-method core, and Theorem 8.1 with the numerical inputs of Theorems 1.5–1.6) covers the complementary range $x \le e^{3100}$ . Without this input the decomposition of the main theorem is incomplete — it is a quoted external result on the same footing as the two numerical verifications, and is listed here for graph fidelity so that the reduction of TaoFivePrimes.five_primes to its inputs is faithful to the paper.

Like the numerical verifications, this is not a tractable formalization target by itself: its proof is a large explicit computation. (Helfgott's 2013 proof of the full ternary Goldbach conjecture supersedes it mathematically but is far larger.)

Preamble

import Mathlib

Formal statement

namespace TaoFivePrimes

theorem liu_wang_three_primes (n : ℕ) (hodd : Odd n) (hn : Real.exp 3100 ≤ (n : ℝ)) :
    ∃ p₁ p₂ p₃ : ℕ, p₁.Prime ∧ p₂.Prime ∧ p₃.Prime ∧ p₁ + p₂ + p₃ = n := by
  sorry

end TaoFivePrimes

Source

M.-C. Liu and T. Wang, On the Vinogradov bound in the three primes Goldbach conjecture, Acta Arithmetica 105 (2002), no. 2, 133–175, Theorem 1; quoted in T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014), Section 1 (the range x > exp(3100))

View graph

Liu–Wang: every odd n≥e3100n \ge e^{3100}n≥e3100 is a sum of three primes

Liu–Wang: every odd $n \ge e^{3100}$ is a sum of three primes