Bounded Gaps Between Primes, Formalized in Lean 4 AI-assisted The Lean 4 proofs were produced by AxiomProver, Axiom Math's AI system for mathematical research through formal proof, then curated and librarized by hand.
A complete, machine-checkable proof that $p_{n+1} - p_n \leq 246$ for infinitely many $n$.
The Twin Prime Conjecture asserts that infinitely many pairs of primes differ by $2$. That remains open, but following the breakthroughs of Yitang Zhang and James Maynard, the Polymath8b collaboration established that infinitely many pairs of primes differ by at most $246$. This project formalizes that result in Lean 4: the whole argument, from Maynard's multidimensional sieve through the enlarged-simplex refinement and numerical certificate of Polymath8b, is now a machine-checked theorem built on Mathlib and on Kontorovich and Tao's PrimeNumberTheoremAnd.
The proof draws on two papers. We formalize Maynard's Small gaps between primes in detail — the multidimensional sieve, the variational quantity $M_k$, and the deduction of $H_1 \leq 600$ — together with the portion of the Polymath8b paper Variants of the Selberg sieve needed for the bound $246$: the enlarged-simplex refinement and the numerical certificate.
The two sources are unified into a single blueprint. Every definition, lemma, and theorem carries a label, a precise statement, and a list of the earlier results it depends on, which yields a dependency graph that both orders the formalization effort and makes the finished proof navigable. The resulting Lean code was produced by AxiomProver, then reviewed and organized into PrimeGapsLib, a library structured so that its pieces can be reused beyond this single theorem.
How the formalization was built
- Write the blueprint Restate the Maynard and Polymath8b arguments as a single unified blueprint, giving every definition, lemma, and theorem a label, a precise statement, and its dependencies. This produces a detailed dependency graph relating all the entities in the proof.
- Formalize with AxiomProver AxiomProver, Axiom Math's AI system for mathematical research through formal proof, produces machine-checkable Lean 4 proofs of the blueprint's nodes, built on Mathlib and on Kontorovich and Tao's PrimeNumberTheoremAnd.
- Curate and librarize Review the resulting code and organize it, with in-house tooling, into PrimeGapsLib — deduplicating parallel developments and stating results at the generality their consumers actually need.
Sources and scope
-
James Maynard, Small gaps between primes, Annals of Mathematics 181 (2015), 383–413.The multidimensional sieve, the variational quantity $M_k$, and the deduction of $H_1 \leq 600$.
-
D. H. J. Polymath, Variants of the Selberg sieve, and bounded intervals containing many primes, Research in the Mathematical Sciences 1 (2014).The enlarged-simplex refinement and the numerical certificate. The other results in Polymath8b are not part of this project.
Press and coverage
The project was carried out by a large team of mathematical and engineering contributors at Axiom Math; the full author list and citation information are on the project site.