Formalizing progress
toward Goldbach.
A Lean 4 project advancing the formal study of Goldbach’s conjecture, from Chen’s 1+2 theorem toward 1+1.9 and stronger results.
- Formalized
- Chen’s 1+2 theorem
- Work in progress
- The 1+1.9 target
- Longer-term direction
- Stronger results toward Goldbach
Completed result · Chen’s 1+2 theorem
Every sufficiently large even natural number is the sum of a prime and either a prime or a product of two primes.
The two factors may be equal. The proof establishes the existence of a threshold above which every even natural number has such a representation.
Read the exact Lean statement →Explore the development
The mathematical view
Lean Blueprint
Read the outline of the completed 1+2 proof and explore the dependency graph of selected declarations, with links to their Lean source.
Explore the dependency graph →The formal development
Lean Doc
Browse the generated Lean documentation for all four project libraries. Search declarations, inspect their types and follow imports and source links.
Open Chen’s theorem →More than existence
The 1+2 formalization also proves an eventual lower bound for the number of good representations of an even integer. The precise normalization is documented alongside the theorem.
Representation lower bound · Definitions and normalization
For a broader mathematical roadmap, see the proof architecture. The interactive Blueprint shows selected declaration dependencies.
Reproduce the verification
Verify the completed results
From the project root of a checkout of the Lean source snapshot, run these commands using the repository’s pinned toolchain. Use an environment without a LEAN_PATH inherited from another project.
The completed 1+2 theorems use Lean’s standard logical axioms. The verification guide explains the source checks, axiom reports and independent replay.
Verification guide and trust boundary →lake exe cache get
lake --wfail build
python3 scripts/check.py
lake env leanchecker --verbose Goldbach.TheoremSources & reuse
This project builds on UyNewNas/chen-theorem-lean, analytic-number-theory-lean, Mathlib and adapted material from PrimeNumberTheoremAnd.
The 1+2 proof combines modern linear-sieve comparisons, Selberg's upper sieve and proved distribution estimates. See the provenance and mathematical sources for attribution and the role of each component.