Lean formalization of bounded gaps between primes

A formalization of the theorem that $p_{n + 1} - p_{n} \leq 246$ for infinitely many $n$ .

Rohan Aanegola^†, Alberto Alfarano^†, François Charton^†, Evan Chen^*, Ruiz Chen^†, Constantin Eichenberg^†, Srihari Ganesh^†, Tobias Gessler^†, Erik Gregory^†, Leopold Haller^†, Sidharth Hariharan^*, Letong Hong^◇, Vasily Ilin^†, Albert Jiang^†, Yunjiang Jiang^†, Tadeusz Jordan^†, Angus Joshi^†, Andranik Kurghinyan^†, Kenny Lau^*^†, Simon Mahns^†, Rishi Malhotra^†, Bhavik Mehta^*, Michał Mogielnicki^†, Connor Olson^†, Ken Ono^*, Gaurang Pendharkar^†, Bartosz Piotrowski^†, Anish Rajeev^†, Karun Ram^†, Aditya Ramabadran^†, Charlie Ray^†, Guillaume Remy^†, Shubho Sengupta^◇, Ashvin A. Swaminathan^*^†, Jesse Thorner^*, Aleksey Tsaplin^†, Niels Voss^†, Chao Wang^†, Chenkai Wang^†, Yunzhou Xie^*, Jimmy Xin^†, Yinglun Zhu^†

^*Mathematical contributors ^†Engineering contributors ^◇Principal investigators

Read the interactive blueprint

The result

The Twin Prime Conjecture states that there are infinitely many pairs of primes that are two apart, such as $(3, 5)$ , $(5, 7)$ , and $(11, 13)$ . This conjecture is still open, but what we currently know is that infinitely many pairs of primes are separated by no more than $246$ . This was reached through the Polymath8b collaboration after breakthroughs by Yitang Zhang and James Maynard.

Zhang was the first one to give a finite value for a bound, after which Maynard's multidimensional sieve gave the bound $600$ . Polymath8b then brought it down to $246$ , and it is the aim of this project to formalize this result in Lean.

The formalization

The interactive blueprint breaks the argument down into definitions, lemmas, and theorems. It shows what each result depends on and points to the corresponding Lean declaration.

PrimeGapsLib houses a formalization of this result. We formalized the majority of Maynard's paper together with the extension from Polymath8b.

Sources and scope

The proof draws on two papers. We formalize the Maynard argument in detail, but only the portion of Polymath8b used for the bound $246$ .

James Maynard, Small gaps between primes

The multidimensional sieve, the variational quantity $M_{k}$ , and the deduction of $H_{1} \leq 600$ .

Published paper arXiv

D. H. J. Polymath, Variants of the Selberg sieve

The enlarged-simplex refinement and the numerical certificate. The other results in Polymath8b are not part of this project.

Published paper arXiv

How the formalization was built

We first wrote the proof as a blueprint, with a separate entry for each definition and lemma. The dependency graph then gave us an order in which to formalize it.

Create the blueprint and dependency graph

Give every definition, lemma, and theorem a label, a precise statement, and a list of the earlier results it uses. Obtain a detailed dependency graph outlining the relationship between blueprint entities.

Formalize with AxiomProver

AxiomProver is Axiom Math’s AI system for mathematical research through formal proof. It produced machine-checkable Lean 4 proofs built on Mathlib and Kontorovich and Tao's PrimeNumberTheoremAnd.

Curate and librarize the resulting code

Review the AxiomProver code and work with our in-house tooling to organize the AxiomProver code into PrimeGapsLib.

Cite this work

@misc{axiom-prime-gaps,
  author = {Aanegola, Rohan and Alfarano, Alberto and Charton, François and Chen, Evan and Chen, Ruiz and Eichenberg, Constantin and Ganesh, Srihari and Gessler, Tobias and Gregory, Erik and Haller, Leopold and Hariharan, Sidharth and Hong, Letong and Ilin, Vasily and Jiang, Albert and Jiang, Yunjiang and Jordan, Tadeusz and Joshi, Angus and Kurghinyan, Andranik and Lau, Kenny and Mahns, Simon and Malhotra, Rishi and Mehta, Bhavik and Mogielnicki, Michał and Olson, Connor and Ono, Ken and Pendharkar, Gaurang and Piotrowski, Bartosz and Rajeev, Anish and Ram, Karun and Ramabadran, Aditya and Ray, Charlie and Remy, Guillaume and Sengupta, Shubho and Swaminathan, Ashvin A. and Thorner, Jesse and Tsaplin, Aleksey and Voss, Niels and Wang, Chao and Wang, Chenkai and Xie, Yunzhou and Xin, Jimmy and Zhu, Yinglun},
  title  = {Lean formalization of bounded gaps between primes},
  year   = {2026},
  note   = {Interactive Lean formalization blueprint}
}