chen_theorem.toml

id = "chen_theorem"
title = "Chen's theorem"
test = false
module = "LeanEval.NumberTheory.ChenTheorem"
holes = ["chen_theorem"]
submitter = "Kim Morrison"
notes = "Chen's theorem: there are infinitely many primes `p` such that `p + 2` is a prime or a product of two primes (a 'prime or semiprime'). The predicate `HasAtMostTwoPrimeFactors n` is the disjunction 'n is prime' or 'n = a·b with a, b prime'. mathlib has `Nat.Prime` and prime factorization, but no Brun-style weighted sieve."
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. Listed as §224 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Knill, §224."
informal_solution = "Chen's argument is a weighted sieve. Apply Selberg's sieve with a switching device (Chen's 'reversal of roles') to bound from below the number of primes p ≤ x with p+2 having at most two prime factors. The key is a careful estimate of the bilinear error terms via the Bombieri-Vinogradov theorem, which controls primes in arithmetic progressions on average and lets the sieve weight stay positive, forcing infinitely many such p."