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…