Axiom Math's AI System Formalizes Proof of the '246 Theorem' in Prime Number Theory

Axiom Math has used its AI system AxiomProver to automatically verify a machine-checkable proof of the "246 theorem," a result in number theory that the company calls its most significant formalization achievement to date.

The 246 theorem states that there are infinitely many prime pairs differing by no more than 246—the closest mathematicians have come to proving the centuries-old twin prime conjecture, which claims infinitely many primes differ by exactly two. The result came out of the Polymath8b collaboration, which included Fields Medalists James Maynard and Terence Tao, building on Yitang Zhang's 2013 breakthrough that first established a finite bound (70 million) between infinitely many prime pairs. Maynard's subsequent work cut that gap to 600 before Polymath8b brought it down to 246.

Formal verification uses software to check a machine-readable version of a mathematical proof, functioning as a rigorous—though not infallible—check on correctness. A recent incident involving a bug in a formal-verification kernel showed the method can be exploited to accept a false, AI-generated proof, according to a report referenced by IEEE Spectrum. Despite that caveat, automated verification remains one of the strongest available guarantees of proof correctness.

A reusable library, not a one-off result

Axiom Math, led by founding mathematician Ken Ono, has used AxiomProver—described as an autonomous, multi-agent system—to formalize several previously unsolved problems this year, according to the company. Sidharth Hariharan, a Carnegie Mellon Ph.D. student now interning at Axiom Math, says the 246 theorem project differs from prior formalization efforts because its components were built for reuse rather than as a single-use proof.

Earlier this year, rival startup Math, Inc. used its Gauss agent to formalize Maryna Viazovska's 2022 Fields Medal-winning sphere-packing proof. Hariharan, who led human efforts on that formalization blueprint, says Axiom Math's work on the 246 theorem is more comprehensive because it produced a general-purpose library of results on prime gaps—published on GitHub as PrimeGapsLib—with the 246 theorem serving as its flagship result.

Why it matters beyond number theory

The number theory techniques underlying the 246 theorem are foundational to cryptography and cybersecurity, meaning the formalized results could eventually help verify systems that protect digital data, according to Axiom Math.

Ono frames the achievement primarily as a proof of concept for a larger goal: verifying AI-generated software code. He argues that if code properties—such as whether an algorithm terminates or produces correct output for all inputs—can be expressed as precise mathematical statements, tools derived from AxiomProver could formally prove those properties, addressing hallucination and bug risks in AI-written code.

"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."

What this means

This is a research milestone, not a product launch: no new model or API is being released, and Axiom Math has not disclosed pricing, model architecture, or parameter counts for AxiomProver. The genuine significance lies in the strategy shift from one-off formalizations toward reusable proof libraries, which could compound over time the way software libraries do. The stated long-term ambition—using formal verification to check AI-generated code—is speculative and far from demonstrated at scale, but it identifies a real gap: as AI writes more production code, the tools to mathematically certify that code's correctness remain immature. Whether formal methods can scale from pure-math theorems to sprawling, stateful codebases is an open question this work does not yet answer.