Representing a significant milestone in AI-assisted mathematical research, a team at Axiom Math has automatically verified the proof of a theorem relating to prime numbers—colloquially referred to as the “246 theorem”—for the first time using the company’s AI system AxiomProver.
In formal verification, mathematicians task a computer with checking a machine-readable version of a proof. The process is not a 100 percent guarantee that the proof is correct, as a recent demonstration showed, exposing how a bug in the method could be exploited to accept a false, AI-generated proof. Still, the computational method is as close to a rubber stamp as you can get.
This particular verification formalizes an important advance in number theory. Beyond this particular proof, it demonstrates how automated AI verification could be used in the future to ensure the correctness of AI-generated computer code that will soon underlie software across the globe.
Useful formalization by design
This is not AxiomProver’s first rodeo. Axiom Math has used its autonomous, multi-agent system that turns mathematical statements into machine-checkable proofs to crack several unsolved mathematical problems and verify many more proofs this year. But proof formalization of the 246 theorem is by far the most significant, as Ken Ono, Axiom Math’s founding mathematician, explains: “This theorem currently represents the threshold of human knowledge about prime numbers.”
Earlier this year, Axiom Math competitor Math, Inc. used its Gauss agent to formalize Maryna Viazovska’s 2022 Fields Medal-winning proof of the sphere-packing problem in 8 and 24 dimensions. Sidharth Hariharan, a Ph.D. student at Carnegie Mellon University who led human efforts on the blueprint to formalize Viazovska’s proof, says that formalizing the 246 theorem is a more comprehensive and useful achievement.
Now an intern at Axiom Math, Hariharan has been heavily involved in the company’s formalization of the 246 theorem proof. He says that one of the main differences here is that rather than it being a one-shot approach relating to a single problem, Axiom Math has expressly aimed to make components of the formalization reusable for other formalization tasks and mathematical research. The team has wielded AxiomProver to build a library of results about gaps in primes. The 246 theorem is the flagship result within that library.
What is the 246 theorem?
The first few primes are close together: 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, …. And there are several instances where they are separated by a difference of two: 3:5, 5:7, 11:13, 17:19, ….
These pairs of primes are called twin primes. Twin primes become rarer the further you get from zero, but they do still seem to pop up occasionally. The twin prime conjecture, first precisely formulated in the 19th century by French mathematician Alphonse de Polignac, posits that they will keep popping…
Read full article: Axiom Math Uses AI to Formally Verify 246 Theorem
The post “Axiom Math Uses AI to Formally Verify 246 Theorem” by Benjamin Skuse was published on 08/17/2026 by spectrum.ieee.org