AI Used to Verify Toughest Mathematics Proof Yet

Axiom Math has automatically verified the proof of a theorem about prime numbers, colloquially called the "246 theorem," for the first time using its AI system AxiomProver, according to the company. The 246 theorem states that there are infinitely many primes that differ by 246.

Formal verification has a computer check a machine-readable version of a proof. The report notes the process is not a 100 percent guarantee of correctness, citing a recent demonstration in which a bug in the method could be exploited to accept a false, AI-generated proof, though it describes the computational method as close to a rubber stamp.

The 246 result comes from the Polymath8b collaboration. Yitang Zhang, now a professor at Sun Yat-sen University in Guangzhou, China, proved in 2013 that infinitely many pairs of primes are separated by 70 million. University of Oxford professor James Maynard later reduced the gap to 600, work that substantially contributed to his 2022 Fields Medal. Maynard and fellow Fields Medalist Terence Tao of the University of California, Los Angeles, then brought the gap to 246, the closest mathematicians have come to the target gap of two.

Ken Ono, Axiom Math's founding mathematician, said the theorem "currently represents the threshold of human knowledge about prime numbers." 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 Carnegie Mellon University Ph.D. student who led human efforts critical to the Math, Inc. breakthrough and is now an intern at Axiom Math, said Axiom Math's approach is more comprehensive and useful. He said the company aimed to make components of the formalization reusable rather than taking a one-shot approach to a single problem. The team used AxiomProver to build a library of results about gaps in primes, with the 246 theorem as its flagship result.

Ono said he sees proof formalization as a stepping stone to verifying AI-generated code, which is used in systems that run infrastructure, manage finances and protect data. If properties of code, such as whether an algorithm terminates or whether a program's output is correct for any input, can be translated into precise mathematical statements, technologies derived from AxiomProver could be suited to formally stating and proving them, he said. "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 test bed for solving what I think is the most important challenge we will face from AI."