Chen's theorem: every large even $n = p + P_2$

Open

Goldbach.chen_theorem

by jjosh · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

goldbachnumber-theoryprimessieve-theory

There is a threshold $N_0$ such that every even integer $n \ge N_0$ can be written as $n = p + q$ where $p$ is prime and $q$ is either prime or a product of two primes (an almost-prime $P_2$ ).

This is Chen Jingrun's 1966/1973 theorem \u2014 the strongest unconditional result toward the strong Goldbach conjecture, and the canonical demonstration of the parity barrier of sieve theory: weighted sieves cannot distinguish primes from $P_2$ 's once both linear and bilinear error terms are controlled at the level $x^{1/2-\varepsilon}$ . No sieve argument can remove the $P_2$ possibility, so closing Goldbach requires genuinely new input (bilinear estimates beyond the parity barrier, or the circle method in the binary case where its minor-arc information is currently too weak).

Preamble

import Mathlib

Formal statement

namespace Goldbach

theorem chen_theorem :
    ∃ N₀ : ℕ, ∀ n : ℕ, N₀ ≤ n → Even n →
      ∃ p q : ℕ, Nat.Prime p ∧
        (Nat.Prime q ∨ ∃ r s : ℕ, Nat.Prime r ∧ Nat.Prime s ∧ q = r * s)
        ∧ n = p + q := by
  sorry

end Goldbach

Source

J. R. Chen, On the representation of a larger even integer as the sum of a prime and the product of at most two primes, Sci. Sinica 16 (1973), 157-176

View graph

Chen's theorem: every large even n=p+P2n = p + P_2n=p+P2​

Chen's theorem: every large even $n = p + P_2$