AI Startup Axiom Math Formalizes The Closest Proof Yet To The Twin Prime Conjecture

Axiom Math has used its AI system AxiomProver to produce a fully machine-checked formalization of the 'BGP246 theorem,' the best-known bound on small gaps between prime numbers, marking the closest approach yet to the twin prime conjecture. The company released the Lean proof alongside a new open-source library, PrimeGapsLib, designed for reusable infrastructure in prime-gap research. The formalization verifies the 2013 result by Yitang Zhang and subsequent improvements by James Maynard and Polymath8b, which established a gap of 246, conditional on the Bombieri–Vinogradov theorem.

Axiom Math has used https://x.com/axiommathai/status/2089732764279132449?s=20 its AI system AxiomProver to produce a fully machine-checked formalization of what it’s calling the “BGP246 theorem,” the best-known bound on small gaps between prime numbers and the nearest mathematicians have come to settling the twin prime conjecture. The company released the Lean proof alongside a new open-source library, PrimeGapsLib, meant to serve as reusable infrastructure for future work on prime gaps rather than a one-off result that sits unused once the announcement fades. The twin prime conjecture is one of those problems that’s brutally simple to state and has resisted proof since the 19th century. It claims that primes separated by exactly 2, pairs like 3 and 5, or 11 and 13, keep showing up no matter how far out on the number line you go, infinitely often. Nobody has managed to prove this. The real progress has come from a more modest question: is there some fixed gap, not necessarily 2, that infinitely many primes are separated by? For decades that question also went nowhere. Then in 2013, Yitang Zhang, now at Sun Yat-sen University, showed there are infinitely many prime pairs within 70 million of each other. It sounds like a strange number to celebrate, but proving any finite bound exists at all was the breakthrough. Months later, Oxford’s James Maynard used a different technique to crash that gap down to 600, a result that fed into him winning the Fields Medal in 2022. The Polymath8b collaboration, which counted Maynard and UCLA’s Terence Tao among its contributors, pushed it further still, to 246. That number has stood as the world record for twelve years. It’s this result, conditional on the Bombieri–Vinogradov theorem, that AxiomProver has now verified line by line in Lean, the proof assistant that has become the de facto standard for this kind of work. Ken Ono, Axiom Math’s founding mathematician, who left a tenured chair at the University of Virginia to join the startup, called it the current threshold of human knowledge about prime numbers, in comments to IEEE Spectrum. Formal verification is a slower, more mechanical process than ordinary peer review. Instead of a human reading a proof and being convinced by it, every logical step gets translated into code that a computer kernel checks against its axioms, leaving essentially no room for the paper-and-pencil errors that occasionally slip past referees. It isn’t foolproof, as demonstrations of bugs in verification tooling have shown, but it’s the closest thing math has to a guarantee. What Axiom Math is emphasizing this time isn’t just the headline result. The company says it built the formalization so that its components, the lemmas, definitions, and supporting machinery, can be lifted out and reused for other prime-gap research rather than existing only to make BGP246 compile. PrimeGapsLib, which depends on Mathlib and the PNT+ project, is now open for the wider Lean community to build on. Axiom Math is framing this as compounding formalized knowledge instead of leaving each result stranded inside its own repository once the press cycle moves on. The result also lands in the middle of a genuinely crowded stretch for AI-assisted mathematics. Sidharth Hariharan, a Carnegie Mellon PhD student who was central to a rival effort earlier this year, Math, Inc.’s formalization of Maryna Viazovska’s Fields Medal-winning sphere-packing proof using its Gauss agent, is now an intern at Axiom Math and worked on the 246 formalization himself. He’s argued that Axiom’s approach is more comprehensive than what Gauss produced, partly because of that reusability focus. His own group is still working to finish formalizing Viazovska’s proof in full. Axiom Math isn’t alone in racing to attach Lean certificates to big claims. OpenAI recently said its Astra model helped it work through ten open math problems https://officechai.com/ai/openai-says-it-has-solved-10-open-math-problems-using-astra-its-new-model/ , DeepMind’s AlphaProof Nexus has been chalking up solved Erdős problems, and Anthropic’s Fable model was credited with helping disprove the 85-year-old Jacobian conjecture https://officechai.com/ai/an-anthropic-researcher-says-fable-just-helped-him-disprove-the-85-year-old-jacobian-conjecture/ . Lean formalization has increasingly become, as one recent account https://officechai.com/ai/gpt-5-6-sol-helps-prove-that-non-sofic-groups-exist-in-big-math-breakthrough/ put it, the price of entry for a credible math claim rather than an optional extra. Ono’s pitch for why any of this matters beyond number theory is the more interesting part. He sees proof formalization less as an end in itself and more as a testbed for a much bigger problem: verifying AI-generated code. If you can translate a property of a program, that it terminates, that its output is correct for every input, into a precise mathematical statement, then the same machinery that checks a Lean proof can, in principle, check that the code actually does what it claims to. Given how much software is now being written by AI systems, and how little of it is being read line by line by a human before it ships, that’s not a small ambition. “The world is about to run on computer code that nobody has read,” Ono said. Number theory, of all things, underpins the cryptography that keeps that code and the data behind it secure, which gives this particular library an odd kind of double relevance. Whether AxiomProver’s approach actually becomes the reusable foundation Axiom Math wants it to be will depend on whether other researchers start building on PrimeGapsLib rather than just citing the headline number. For now, 246 remains the record, twin primes remain unproven, and the gap between the two is exactly the kind of problem this generation of AI math tools seems determined to keep chipping away at.