goldbach-lean

A Lean 4 project formalizing progress toward Goldbach's conjecture and building reusable analytic number theory, with Chen's 1+2 theorem and Li–Liu's 1+1.9 theorem formalized. Stronger results remain a research direction.

The Li–Liu result proves:

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.

It also proves the strict 0.0004 lower bound for the number of distinct prime first summands satisfying this condition, in the Liu singular-series normalization. The earlier 1+2 result remains available through its original import and public names: every sufficiently large even natural number is a prime plus another prime or a product of two primes, whose factors may be equal.

The release notes describe the new results and retain the historical v1.0.0 record. The recorded build benchmarks measure the v1.0.0-rc1 and v1.0.0 1+2 developments.

Project homepage · Lean API documentation · Interactive proof Blueprint

The Lean API documentation covers all four project libraries, with declaration search, source links, and import navigation. The complete local publication layout includes the Li–Liu mathematical proof structure and paper correspondence at /report/. Optional dependency panels in the Blueprint and API expose the compiled dependency data from internal static assets. See how the website is built and published.

Proof at a glance

The following roadmap describes the Chen 1+2 route. The Li–Liu extension has its own public entry and source route.

flowchart BT
  distribution["Prime distribution and analytic estimates"] --> lower["Weighted lower sieve"]
  comparison["Jurkat-Richert functions and Suzuki comparison"] --> lower
  distribution --> upper["Switched-source Selberg upper sieve"]
  lower --> counting["Finite counting: lower bound minus triple penalty"]
  upper --> counting
  counting --> quantitative["Quantitative representation bound"]
  quantitative --> chen["Chen's theorem: prime + at most two primes"]

This is a mathematical roadmap: arrows point from an input to the result it supports, and may summarize several modules. The source map separates this view from direct imports and compiled declaration dependencies.

The interactive Blueprint renders selected declaration dependencies from LeanArchitect, with links to their Lean source. This curated mathematical view is distinct from the module import graph and the compiled declaration graph available through these panels. Imports record module access; only the separate compiled value references record actual static uses within stored proofs or definitions. The declaration graph also keeps type and recursorRHS references separate.

The release procedure for this documentation update builds and validates the complete static site locally, then publishes it independently to gh-pages from a fresh staging checkout. Lean CI retains the full warning-free build, source/statement/axiom checks, script tests, and replay of Goldbach.Theorem, Goldbach.Checks, Goldbach.OnePlusOneNine, Goldbach.OnePlusOneNineChecks and Goldbach.All; it does not generate or deploy the website. A reused API artifact may document an earlier source version than the website: record both exact revisions and preserve the API's original source links. Follow the deployment procedure and read back the live build records after Pages deploys to determine which version is online.

Main results

The two developments have separate imports over shared analytic foundations. Use import Goldbach for the established 1+2 interface, import Goldbach.OnePlusOneNine for 1+1.9, or import Goldbach.All for both.

import Goldbach.OnePlusOneNine

#check Goldbach.one_plus_one_nine
#check Goldbach.one_plus_one_nine_real
#check Goldbach.one_plus_one_nine_count
#check Goldbach.one_plus_one_nine_lower_bound

The natural-power theorem retains the exact r^10 ≤ q^9 condition; the real-power version states r ≤ q^((19/10 : ℝ) - 1). The count theorem gives (1/2500) * liuSingularSeries N * N / (Real.log N)^2 < D19 N, where D19 counts different eligible primes p. The stronger lower-bound family allows each fixed real κ < 515093/800000000, with a threshold depending on κ. See the precise statements and normalization.

The original Chen interface is unchanged:

import Goldbach

#check Goldbach.chen_theorem
#check Goldbach.representation_lower_bound

Goldbach.chen_theorem proves Goldbach.ChenTheorem. The specification in Goldbach/Statement.lean is deliberately independent of the sieve implementation:

∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N → Even N →
  ∃ p q : ℕ, p.Prime ∧
    (q.Prime ∨ ∃ r s : ℕ, r.Prime ∧ s.Prime ∧ q = r * s) ∧ N = p + q

The quantitative theorem gives an eventual lower bound of 0.67 * liuSingularSeries N * N / (Real.log N)^2 for the cardinality of the actual good-representation set, for even N. See docs/THEOREMS.md for definitions and normalization.

Build and check

Install elan, then run from this directory:

unset LEAN_PATH LEAN_SRC_PATH
lake exe cache get
lake --wfail build
python3 scripts/check.py
lake env lean Goldbach/Checks.lean
lake env leanchecker --verbose Goldbach.Theorem

The toolchain and all Git dependencies are pinned by lean-toolchain and lake-manifest.json. The checkout contains the complete local source closure. lake exe cache get downloads Mathlib's compiled cache; the project proofs are built from source. scripts/check.py runs separate statement and axiom probes for Chen 1+2 and Li–Liu 1+1.9. Goldbach/Checks.lean retains the Chen checks; Goldbach/OnePlusOneNineChecks.lean checks the new interface. The leanchecker command above replays the Chen public module against cached imports. The verification guide gives the Li–Liu inspection and replay commands as well.

The checks reject proof placeholders and custom axioms in the shipped source, verify the public theorem axiom reports against Lean's standard classical axioms (propext, Classical.choice, Quot.sound), and check source hygiene. Read docs/VERIFICATION.md for the exact coverage and limitations.

Focused builds and upgrading an existing checkout

lake build Goldbach.Theorem          # Chen 1+2
lake build Goldbach.OnePlusOneNine   # Li–Liu 1+1.9
lake build Goldbach.All              # both public interfaces
lake build                          # full project

If you have already built the project, keep .lake/ and update your checkout without cleaning it. To update an existing main checkout:

git switch main
git pull --ff-only
lake build Goldbach.OnePlusOneNine

To use the integration branch instead, run git fetch origin, then git switch integrate/liliu19-latest. If that branch is not yet local, use git switch --track origin/integrate/liliu19-latest instead. Preserve or commit any local work before switching branches.

The package configuration, toolchain and dependency pins are unchanged. Lake can reuse unchanged dependency artifacts and rebuilds new or changed modules and affected consumers as needed. Keep the existing .lake/ directory; rebuild work depends on your cache state and selected target.

Organization

• Goldbach/: independent statement, public theorems, and acceptance checks.
• MathlibNt/: Chen and Li–Liu sieve and analytic proof implementations.
• AnalyticNumberTheory/: reusable prime-distribution, Mertens, and sieve results.
• PrimeNumberTheoremAnd/: the attributed, adapted prime-number-theorem source closure.
• scripts/: reproducible source and trust checks.
• docs/: theorem map, architecture, provenance, and verification instructions.

The proof uses a modern combination of Jurkat–Richert/Richert linear sieve, Suzuki comparison results, Selberg upper sieve, and proved distribution bounds. The architecture guide explains how these ingredients combine to prove the public results.

Sources and license

Distributed under Apache-2.0. Upstream copyright notices are retained. This project builds on UyNewNas/chen-theorem-lean, UyNewNas/analytic-number-theory-lean, Mathlib, and the adapted source closure of AlexKontorovich/PrimeNumberTheoremAnd. Attribution is described in docs/PROVENANCE.md.