Bounded prime gaps improved to 212, with a Lean certificate of the deduction
Nine authors prove that infinitely many pairs of primes differ by at most 212, improving Stadlmann's 240, with the deduction certified in Lean by the group's own prover.
- Lab
- Axiom Math
- Model
- AxiomProver
- Field
- Mathematics
- Date
- 2026-09-03
- Human collaborators
- Francois Charton, Letong Hong, Kenny Lau, Ken Ono, Guillaume Remy, Ho Chung Siu, Ashvin A. Swaminathan, Jesse Thorner, Yunzhou Xie
- Problem posed
- 1849 · open 177 yrs
Sources
Original work
Independent commentary
What was found
The bounded-gaps line runs from Zhang in 2013 through Maynard's sieve to the Polymath8b bound of 246, which this registry already carries as a formalization entry, and then to Stadlmann's 240. This paper builds on Stadlmann's work to reach 212. The authors are explicit about the division of labour: the mathematics is theirs, and AxiomProver generated the Lean certificate of the deduction from natural-language specifications rather than finding the argument.
Novelty check
The bound improves on published work the paper names in its own abstract: 246 from Polymath8b and 240 from Stadlmann. No earlier claim below 240 was found in the four registries. Two competing prime-gap claims appeared in the same window, an unreviewed 236 with no named model and no preprint, and an OpenAI 186 that is recorded separately here and is conditional on three unproved axioms; neither displaces this one on evidence.
Caveats and known objections
Nothing outside the author group has checked this. The certificate covers the deduction from stated assumptions rather than the analytic inputs themselves, the same shape as the 246 entry already in the registry, so it is not a machine-checked proof of the bound from first principles. The Lean build was not independently reproduced for this entry. Autonomy is collaborative on the authors' own framing, that the mathematics is theirs and the AI contribution is the formal certificate. Whether this should supersede or extend 2026-08-18-prime-gaps-246 rather than sit beside it is an open editorial question: same lab, same tooling, a strictly better bound.
Also recorded at
vibemathedbounded-prime-gaps-at-most-212
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
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 Claimed and Collaborative.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and collaborative for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Bounded prime gaps improved to 212, with a Lean certificate of the deduction. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-03-prime-gaps-212BibTeX
@misc{whataifound-axiommath-2026-212,
title = {Bounded prime gaps improved to 212, with a Lean certificate of the deduction},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Axiom Math. Verification: Claimed. Autonomy: Collaborative.},
url = {https://whataifound.org/finding/2026-09-03-prime-gaps-212}
}