Formalizing progress
toward Goldbach.
A Lean 4 project advancing the formal study of Goldbach’s conjecture and reusable analytic number theory, with Chen’s 1+2 and Li–Liu’s 1+1.9 theorems formalized and stronger results as a research direction.
- Formalized
- Chen’s 1+2 theorem
- Formalized
- Li–Liu’s 1+1.9 theorem
- Longer-term direction
- Stronger results toward Goldbach
Completed result · Li–Liu’s 1+1.9 theorem
Every sufficiently large even natural number has a representation N = p + r*q, where p and q are prime, r = 1 or r is prime, and r^10 ≤ q^9.
The factor-size condition is stated in exact natural-number arithmetic. The real-power endpoint gives the equivalent condition r ≤ q^(9/10).
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
Li–Liu proof structure
Begin with the exact counted object and normalization. Follow the four public interfaces into their two proof routes, then compare the paper's stages with the implemented finite counts, distribution inputs and integral certificates.
Read the paper-to-Lean correspondence →The mathematical view
Lean Blueprint
Start with the counting objects and mathematical reductions, then follow the sieve estimates, error control and final positive bounds. Each proof chapter connects its explanation to selected implemented lemmas; this is the explanatory projection of the wider development.
Open the mathematical overview →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 →Shared foundations,
independent routes
Prime-distribution estimates, sieve comparisons and exact finite counting support the two developments. The Blueprint explains which source and local density each estimate applies to, how its errors are controlled, and where the two proof routes differ.
Reusable transport and integration lemmas support those mathematical stages. Each theorem keeps its own counting predicate, factor ranges and public interface, while the shared proofs form a reusable analytic number theory library.
Follow the foundations into both proof routes →More than existence
The Li–Liu count D19(N) counts distinct eligible primes p, once per prime. For every sufficiently large even N, it is strictly greater than (1/2500) * liuSingularSeries(N) * N / log(N)^2, with 1/2500 = 0.0004 exactly.
A stronger family gives the eventual lower bound with each fixed real coefficient κ < 515093/800000000; the threshold is chosen after κ. The Chen 1+2 bound retains its coefficient 0.67 for its own good-representation count. Both use the Liu singular-series normalization.
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.
Both completed developments use Lean’s standard logical principles, with no unproved mathematical premise in their public dependency cones. The verification guide explains the separate Chen and Li–Liu acceptance probes, endpoint inspection and module replay.
Verification guide and trust boundary →lake exe cache get
lake build Goldbach.Theorem
lake build Goldbach.OnePlusOneNine
lake build Goldbach.All
lake --wfail buildKeep your existing build
Import Goldbach for 1+2, Goldbach.OnePlusOneNine for 1+1.9, or Goldbach.All for both. The original 1+2 entry remains separate from the new extension.
The package configuration, toolchain and dependency pins are unchanged. Keep .lake/ when updating; Lake reuses unchanged dependency artifacts and rebuilds new or affected modules as needed. See the upgrade commands.
Sources & reuse
This project builds on UyNewNas/chen-theorem-lean, analytic-number-theory-lean, Mathlib and adapted material from PrimeNumberTheoremAnd.
The developments combine linear-sieve comparisons, Selberg's upper sieve, proved distribution estimates and Li–Liu's constrained finite counts and integral bounds. See the provenance and mathematical sources for attribution and the role of each component.