Bounded prime gaps of 246 formalized in Lean from Bombieri-Vinogradov
A machine-checked Lean development proves that infinitely many pairs of primes differ by at most 246, taking the Bombieri-Vinogradov theorem as a hypothesis rather than proving it.
- Lab
- Axiom Math
- Model
- AxiomProver
- Field
- Mathematics
- Date
- 2026-08-18
- Human collaborators
- Evan Chen, Sidharth Hariharan, Kenny Lau, Bhavik Mehta, Ken Ono, Ashvin Swaminathan, Jesse Thorner, Yunzhou Xie
Sources
Original work
Announcement
Media coverage
What was found
The 246 bound is the closest mathematics has come to the twin prime conjecture: Zhang broke the bounded-gaps barrier in 2013, Maynard's multidimensional sieve brought it to 600, and the Polymath8b collaboration tightened that to 246 in 2014. This project formalizes the majority of Maynard's paper together with the Polymath8b extension, in Lean 4 on top of Mathlib and the PrimeNumberTheoremAnd development led by Kontorovich and Tao. AxiomProver generated machine-checkable proofs which human formalisers at Axiom Math then curated and librarized into PrimeGapsLib, released as reusable infrastructure. The mathematics is not new; the machine-checked proof of it is.
Novelty check
The theorem is not new and the project does not claim it is. H at most 246 is Polymath8b, 2014, building on Maynard 2013 and Zhang 2013, and all three are cited by the project as the sources being formalized. What did not previously exist is a machine-checked proof: no formalization of the Maynard sieve or the Polymath8b bound appears in Mathlib or in the Lean community's project index before this, and the related PrimeNumberTheoremAnd project it builds on formalizes a different theorem. This entry records a formalization milestone, in the same sense as the strong prime number theorem entry, not a new mathematical result.
Caveats and known objections
The formalization is not self-contained. Palomar registered the development under the theorem names bombieriVinogradov_implies_prime_gap_le_246 and bombieriVinogradov_implies_nth_prime_gap_le_246, and Palomar's own record describes the flagship result as conditional on the Bombieri-Vinogradov theorem, which is assumed as a hypothesis because it is not yet in Mathlib. Bombieri-Vinogradov has been a theorem since 1965, so the mathematics is unconditional in the literature and only the Lean development is conditional, but the project's public page states the 246 result without that qualification, and the two readings should not be conflated. Beyond the mechanical Palomar check there has been no mathematical peer review of the formalization choices. Autonomy graded collaborative: the disclosure is that the proof was generated collaboratively between human formalisers and AxiomProver, with humans curating and librarizing, and roughly 41 named contributors are credited.
Machine-checked elsewhere
PalomarPALOMAR-2026-08-18-000002
AxiomMath/PrimeGapsLib at 1faa7b14e82d · checked 2026-08-18
ProvedbombieriVinogradov_implies_prime_gap_le_246bombieriVinogradov_implies_nth_prime_gap_le_246
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review.
Registered the day Palomar opened for submissions. The theorem names are where the Bombieri-Vinogradov hypothesis is visible; the project's own page does not carry that qualification.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and Collaborative.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and collaborative for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Bounded prime gaps of 246 formalized in Lean from Bombieri-Vinogradov. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-18-prime-gaps-246BibTeX
@misc{whataifound-axiommath-2026-246,
title = {Bounded prime gaps of 246 formalized in Lean from Bombieri-Vinogradov},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Axiom Math. Verification: Formally verified. Autonomy: Collaborative.},
url = {https://whataifound.org/finding/2026-08-18-prime-gaps-246}
}