The literal statement of Chen's theorem

This specification uses only natural-number primality, parity, addition, and multiplication. It does not use any project-specific almost-prime predicate. The two factors in the composite case are allowed to coincide.

def Goldbach.ChenTheorem : Prop

Every sufficiently large even natural number is a prime plus either a prime or a product of two primes. The threshold is existential, not explicit.

Equations

• Goldbach.ChenTheorem = ∃ (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