AI System Verifies the 246 Theorem, a Milestone in Prime Number Research

A team at Axiom Math has automatically verified the proof of the 246 theorem — the strongest result to date on the gaps between prime numbers — using its AI system AxiomProver, the first machine-checked formalization of the result.

The theorem states that there are infinitely many primes that differ by exactly 246. It marks the closest mathematicians have come to the twin prime conjecture, the centuries-old unsolved claim that infinitely many primes differ by two. Ken Ono, Axiom Math's founding mathematician, put the result in blunt terms: "This theorem currently represents the threshold of human knowledge about prime numbers."

Formal verification works by tasking a computer with checking a machine-readable version of a proof. The method is not infallible — a recent demonstration showed how a bug in the verification process could be exploited to accept a false, AI-generated proof — but it remains the closest thing mathematics has to a rubber stamp.

Built to be reused

This is not AxiomProver's first result. Axiom Math has used the autonomous, multi-agent system, which turns mathematical statements into machine-checkable proofs, to crack several unsolved problems and verify many more proofs this year. But the 246 theorem formalization stands apart in scope and intent.

Earlier this year, competitor Math, Inc. used its Gauss agent to verify 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 the human efforts critical to that breakthrough, says Axiom Math's approach to the 246 theorem is more comprehensive and useful. His group continues to work toward fully formalizing Viazovska's proof.

Hariharan is now an intern at Axiom Math and has been heavily involved in the 246 theorem formalization. The key difference, he says, is design: rather than a one-shot verification of a single problem, Axiom Math built components meant to be reused in other formalization tasks and mathematical research. The team used AxiomProver to construct a library of results about gaps in primes, with the 246 theorem as its flagship result.

Why 246 matters

The first primes cluster tightly: 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31. Some pairs — 3 and 5, 5 and 7, 11 and 13, 17 and 19 — differ by exactly two. These are the twin primes. They grow rarer the further out you go on the number line, but they keep appearing.

The twin prime conjecture, precisely formulated in the 19th century by the French mathematician Alphonse de Polignac, posits that twin primes never stop: there are infinitely many. Despite its simple statement, the conjecture remains unproven.

The first real progress came only in 2013, when Yitang Zhang, now a professor at Sun Yat-sen University in Guangzhou, China, proved that infinitely many pairs of primes are separated by 70 million. A few months later, University of Oxford professor James Maynard used a different technique to cut the gap from 70 million to just 600 — a feat that contributed substantially to his 2022 Fields Medal, widely regarded as the Nobel Prize of mathematics.

Maynard and fellow Fields Medalist Terence Tao, a professor at UCLA, then brought the bound down to 246 through the Polymath8b collaboration. That is the result AxiomProver has now verified.

From proofs to verified code

The techniques formalized in this work matter beyond number theory circles. Number theory underpins all present-day cybersecurity and cryptography, and the verified methods could eventually help check specific mechanisms used to protect digital data.

Ono is focused on a bigger prize. He sees formal proof verification as a stepping stone to verifying AI-generated code, which is already entering systems that run infrastructure, manage finances, and safeguard data — despite well-documented problems with hallucinations, bugs, and unintended vulnerabilities.

The connection is direct. If properties of code, such as whether an algorithm terminates or whether a program produces correct output for any input, can be translated into precise mathematical statements, then technologies derived from AxiomProver would be well suited to state and prove them formally. A mathematical guarantee of correctness would make AI-generated code safe to deploy.

"The world is about to run on computer code that nobody has read," Ono concludes. "AI is here and we can no longer look away — proof formalization is a test bed for solving what I think is the most important challenge we will face from AI."

With the prime-gaps library now public and reusable, the 246 theorem verification is less an endpoint than a template: each additional formalized result widens the base that future verification systems — for theorems and for software alike — can build on.