The gap between AI systems that ace math competitions and AI systems that do research mathematics just got noticeably narrower. Axiom Math said Monday that its AxiomProver produced a machine-checked proof of the strongest known result about gaps between prime numbers, a milestone first reported by IEEE Spectrum.
The claim: infinitely many prime pairs sit within 246 of each other. That number is the sharpest bound the mathematical community has reached in the long pursuit of the twin prime conjecture, which holds that primes separated by exactly two recur without end. Axiom’s blueprint lists 41 named contributors and formalizes work by James Maynard, whose 2013 sieve methods produced the 600 bound, plus the Polymath8b effort that later squeezed it to 246.
The proof lives in Lean 4, a language checked line by line by a small trusted program, so no human referee’s judgment is in the loop. Earlier AI milestones mostly stopped at olympiad-style problems with short, self-contained solutions; formalizing a research result carries far more definitions, dependencies, and edge cases.
Axiom’s workflow starts with a blueprint that labels every definition, lemma, and theorem and maps their dependencies. AxiomProver then generates proofs on top of the community Mathlib library, and human reviewers assemble the output into a public repository called PrimeGapsLib.
The company’s founding mathematician, Ken Ono, described the 246 bound as the current threshold of knowledge about primes. The repository also covers Maynard’s earlier 600 result and includes an empty proof slot, so outsiders can run the Lean checker themselves and confirm the work independently.
