AI agents turn the longest mathematical proof ever into checkable code in 24 days

Mathematicians have called it "the enormous theorem" for decades: the classification of finite simple groups. Its proof is the longest in the history of mathematics. It runs to about 15,000 pages, spread over more than 500 papers by around a hundred mathematicians. No single person can check all of it. On 26 October, the AI company Axiom Math reported that it has now had the work checked by a computer, step by step.

In 24 days, dozens of AI agents translated the whole proof into Lean, guided by engineers and mathematicians at Axiom. Lean is a programming language for mathematics: every definition and every step is written down so precisely that software can check whether it is correct. The result is about 43.1 million lines of code. Axiom is making that code public on GitHub, so anyone can have it checked themselves.

What the theorem says

In mathematics, groups are the language of symmetry. A square tile, for example, can be turned a quarter turn or flipped over without looking any different. All those moves together form a group. Finite simple groups are the building blocks from which all finite groups are made, just as molecules are made of atoms. The theorem says that there are only a few kinds of these building blocks: a handful of families that go on forever, plus exactly 26 outsiders. The largest outsider is called the Monster group. It has about 8 × 10^53 elements, a number with 54 digits.

The proof has a long history. The classification was announced as complete in 1983. Yet a gap remained, which was only closed in 2004 with a 1,221-page work by Michael Aschbacher and Stephen Smith. Mathematicians have also been working for years on a new, clearer version of the proof. By 2023, ten of its at least twelve volumes had appeared.

Errors found and repaired

Because the computer takes nothing for granted, it also turned up places where the published proof was not quite right. Axiom counts 34 noteworthy deviations from what is in the mathematical literature. The most important one was in a 1986 proof that is part of the classification. The agents found concrete counterexamples to one of its claims. Closing that gap needed a new piece of mathematics, which Axiom is publishing as a separate paper. With these repairs, the whole proof has now been approved by the computer.

Axiom consulted Richard Lyons and Ronald Solomon, two group theorists who worked on the original classification and sit on the company's advisory board. The company is also publishing a list of corrections, so other mathematicians can build on it.

The work was split into 108 milestones and about 380 smaller tasks. The results come from Axiom itself. Because the code is public, other mathematicians can now check whether everything is correct. They will look especially at whether the definitions in Lean say exactly the same as in the human proof.

New proofs and old proofs

This month, OpenAI and Anthropic also reported that their AI models had solved major mathematical problems, with proofs that a computer has already checked. There, the AI itself found something new. Axiom shows that AI can also do the reverse: check an existing human proof that is too big to check by hand from start to finish, and improve it where needed.

What does this mean for the road to the singularity?

AI can now deliver work on a scale that no human team can get through, and a computer can check that work down to the smallest step. That matters: the more AI comes up with by itself, the more important it becomes that we can check whether it is right without having to take everything on trust. The enormous theorem shows that this also works for a proof of 15,000 pages, and that AI does not only check existing human knowledge but also makes it better. The next step is for mathematicians to check the public code themselves.

What is the technological singularity? Read the explanation →