Project home · Lean Doc · Li–Liu proof structure

1 Two counting theorems and their proof routes ▶
2 Prime distribution and sieve foundations ▶
- 2.1 Analytic foundations of the two Goldbach arguments
3 Chen: a prime plus at most two primes ▶
- 3.1 Chen’s theorem: from a signed sieve weight to representations
4 Li–Liu: two factors with a prescribed imbalance ▶
- 4.1 Li–Liu’s asymmetric Goldbach theorem
5 Reading the formal implementation ▶
All documented lemmas — proof graph
Two counting theorems and their proof routes — proof graph
Prime distribution and sieve foundations — proof graph
Chen: a prime plus at most two primes — proof graph
Li–Liu: two factors with a prescribed imbalance — proof graph

goldbach-lean: Chen and Li–Liu theorems

goldbach-lean contributors

1 Two counting theorems and their proof routes
2 Prime distribution and sieve foundations
- 2.1 Analytic foundations of the two Goldbach arguments
3 Chen: a prime plus at most two primes
- 3.1 Chen’s theorem: from a signed sieve weight to representations
4 Li–Liu: two factors with a prescribed imbalance
- 4.1 Li–Liu’s asymmetric Goldbach theorem
5 Reading the formal implementation