Axiom Math says its AxiomProver system has produced a machine-checked Lean 4 proof of the strongest known result on gaps between prime numbers: the theorem that infinitely many pairs of primes differ by no more than 246. The company published the result on August 17, 2026 as an interactive formalization blueprint credited to 41 named mathematical, engineering, and principal-investigator contributors, with IEEE Spectrum first reporting the milestone.
The 246 bound is the current edge of human knowledge in the long attack on the twin prime conjecture, the 19th-century hypothesis that primes separated by exactly two recur forever. Axiom Math’s project page describes the work as a unified formalization of James Maynard’s 2013 paper “Small gaps between primes” together with the portion of the Polymath8b collaboration’s follow-up that tightened Maynard’s bound of 600 down to 246. The machine-checked proofs are organized into a public Lean library, PrimeGapsLib, with the 246 theorem as its flagship result.
“This theorem currently represents the threshold of human knowledge about prime numbers,” said Ken Ono, Axiom Math’s founding mathematician.
Formal verification means translating a proof into a language a small, trusted program called a kernel can check line by line. The result is not an absolute guarantee — the statement itself has to be translated correctly, and the checker has to be sound — but it removes the human referee’s fallibility from the chain. Until now, AI systems that compete on mathematics benchmarks have mostly been measured on competition problems with short, self-contained proofs; the gap between those results and research-level formalization has been wide, a pattern visible in earlier systems that excelled at olympiad geometry while leaving research mathematics largely untouched.
From 70 Million to 246
The conjecture itself, precisely formulated by Alphonse de Polignac in the 19th century, remains unproven. The first finite bound of any kind came in 2013, when Yitang Zhang proved that infinitely many prime pairs fall within 70 million of each other. Months later, Maynard introduced a refined sieve method and cut the bound to 600 — work that contributed to his 2022 Fields Medal — and the Polymath8b collaboration, which included Maynard and Terence Tao, pushed it to 246. Axiom Math’s blueprint lays that progression out as the project it set out to formalize.
The formalization follows a pipeline the company describes in three stages. Researchers first wrote the proof as a blueprint — every definition, lemma, and theorem given a label, a precise statement, and a list of the results it depends on — producing a dependency graph that ordered the work. AxiomProver, the company’s multi-agent system for mathematical research through formal proof, then generated machine-checkable Lean 4 proofs built on Mathlib, the community mathematics library, and on PrimeNumberTheoremAnd, the existing formalization project led by Alex Kontorovich and Tao. Axiom’s team then reviewed the generated code and organized it into PrimeGapsLib.
The library’s stated main results go slightly beyond the headline theorem. Alongside the 246 bound, it formalizes Maynard’s 600 bound, and it includes a self-contained verification challenge — built only on Mathlib, with the proof slot left empty — that lets anyone with the Lean comparator tool independently confirm that the library’s proofs match the stated theorems. The company warns that the full check can take hours; a reduced version covering the other two results runs in minutes.
Where This Sits Among AI Formalization Claims
The result lands in a year of escalating claims about AI systems doing research-grade mathematics, most of them anchored to competition scores or short proofs. Axiom Math has been one of the more aggressive claimants: AxiomProver is credited with solving previously open problems, including work the company has placed in peer-reviewed journals, and AI systems have now solved several long-standing Erdős problems. The 246 formalization is a different kind of result — not a new theorem, but a machine-checked reconstruction of one of the most technically demanding proofs in modern number theory.
The closest comparison is earlier this year, when Math, Inc. used its Gauss agent to complete the formal proof of Maryna Viazovska’s Fields Medal-winning sphere-packing results in dimensions 8 and 24. Sidharth Hariharan, the Carnegie Mellon Ph.D. student who led the human blueprint effort on that formalization and is now an intern at Axiom Math and a named mathematical contributor on the 246 project, argues the new result is the more comprehensive achievement. His reasoning, as he described it, is that Axiom built for reuse: rather than a one-shot formalization of a single proof, PrimeGapsLib is a maintained library of prime-gap results meant to support future formalization work and research.
That distinction matters for how the result should be read. A one-off verification demonstrates that a system can survive contact with one hard proof. A library demonstrates something closer to infrastructure — reusable formal machinery that other results can build on — which is the direction formal proving systems have been moving as they shift from solving exercises to checking real mathematics. The capability claim here rests on artifacts that are public and re-runnable rather than on a benchmark score: the blueprint, the Lean code, and a comparator challenge designed so outside researchers can verify the proofs themselves.
Ono frames the mathematics as a testbed for a larger ambition. If properties of software — whether a program terminates, whether its output is correct for every input — can be expressed as precise mathematical statements, then systems derived from AxiomProver could formally prove them, he argues, pointing toward verification of the AI-generated code beginning to run infrastructure, finance, and security systems.
“The world is about to run on computer code that nobody has read,” Ono said. “AI is here and we can no longer look away—proof formalization is a testbed for solving what I think is the most important challenge we will face from AI.”
For now the deliverable is narrower and checkable: a 41-author blueprint, a public Lean library, and a machine-verified proof that primes within 246 of each other never run out — the twin prime conjecture’s closest verified neighbor, and the deepest piece of research mathematics an AI system has yet checked end to end.
