Axiom Math announced that its AI system AxiomProver has formally verified the "246 theorem" — one of the toughest results in number theory ever formalized. It is the closest proof yet toward the twin prime conjecture, and the machine checked its correctness step by step.
Key takeaways
- Axiom Math formalized the "246 theorem" with its AxiomProver system.
- The theorem: there are infinitely many prime pairs at a gap of 246.
- Original proof: James Maynard and Terence Tao (the Polymath8b project).
- AxiomProver is an autonomous, multi-agent system that turns statements into machine-checkable proofs.
- It produced a reusable PrimeGapsLib library released on GitHub.
Closest to twin primes
The twin prime conjecture says there are infinitely many prime pairs differing by 2 (like 11 and 13). Nobody has proven it. The "246 theorem" is the closest foothold: it proves infinitely many pairs at a gap of at most 246.
The result came out of the Polymath8b project, which cut the bound from 70 million (2013) through 600 down to 246 — building on work by Fields Medalists James Maynard and Terence Tao. This is a real, deep piece of modern mathematics, not a toy example.
Symbol meaning
- …
- gap between consecutive primes
- …
- the value the gaps return to infinitely often
| Stage | Max gap |
|---|---|
| 2013 — first result | 70,000,000 |
| 2013 — further work | 600 |
| 246 theorem | 246 |
This theorem currently represents the threshold of human knowledge about prime numbers.
Ken Ono, founding mathematician at Axiom Math.
How AxiomProver works
AxiomProver is an autonomous, multi-agent system that turns mathematical statements into machine-checkable proofs — a process called autoformalization. Rather than trusting a human reviewer not to miss an error, formal verification gives machine-confirmed certainty for every step.
At this scale it is AxiomProver's most significant achievement to date. The work involved Sidharth Hariharan, a Carnegie Mellon University Ph.D. student and Axiom Math intern. The result is not only the proof itself but also the reusable PrimeGapsLib library on GitHub for others to use.
Why it matters
Formally verifying a hard theorem shows AI maturing from a generator of plausible answers into a tool that delivers hard, checkable certainty.
That matters beyond mathematics: the same techniques could one day prove the correctness and safety of code — including code written by AI. In a world where more and more software is machine-generated and nobody reads all of it, a formal proof becomes one of the few reliable ways to keep control.
What's next?
- The PrimeGapsLib library is available on GitHub and can seed further formalizations in number theory.
- Axiom Math points to verifying AI-generated code as the target application of these techniques.
- The next test will be formalizing results even closer to the twin prime conjecture.
Sources
- IEEE Spectrum — AI Used to Verify Toughest Mathematics Proof Yet
- Wikipedia — Twin prime conjecture
