AI Agents Checked Maths’ Longest Proof, 15,000 Pages, in 24 Days

The longest proof in mathematics runs to about 15,000 pages, spread over more than 500 articles by roughly 100 mathematicians. A start-up called Axiom says swarms of AI agents turned it into 43.1 million lines of computer-checkable code in 24 days. Along the way they found 34 places where the published maths did not match what was claimed. If it holds up, it is the clearest sign yet that AI can do huge amounts of checkable work, not just write plausible text.

The number, and what it means

Axiom published the work on its research blog, dated 26 October, and put the code in a public GitHub repository. Its project site lists 43.1 million lines of code and 2.05 million separate definitions and results, drawn from 715 papers and books.

In plain terms, the company says it has taken one of the great achievements of 20th-century mathematics, written over several decades by about 100 people, and rewritten every step in a form a computer can check without trusting anyone.

Axiom says the project began on 1 October with a single chat channel and a plan of 108 milestones and about 380 smaller tasks. The first agents went to work on 2 October. That makes it roughly four weeks from start to finish, for a body of work that took humans decades to write and then decades more to tidy up.

What was being proved

The theorem is called the Classification of Finite Simple Groups. A group, in maths, is a set of moves that describe symmetry. Axiom’s own example is a cube: there are 24 ways to turn it so it looks exactly as it did before. Groups can be broken down into basic pieces, the way molecules break down into atoms. The “simple” groups are those atoms.

The classification is a complete list of them, a kind of periodic table of symmetry. It says every one belongs to a few known families or is one of exactly 26 odd ones out. The largest of those, called the Monster, has roughly 8 followed by 53 zeros elements. The hard part is not listing the groups. It is proving that nothing is missing.

Mathematicians declared the job finished in 1983. It was not. One gap stayed open until a 1,221-page treatment appeared in 2004, and other fixes followed in 2008. A second, cleaner version of the proof has filled ten volumes since the late 1980s and is still not complete, according to Axiom’s account. One of the leading group theorists, Michael Aschbacher, wrote in 2005 that “it is impossible to write out a very long and complicated argument without error.”

How the AI did it

The tool at the centre is Lean, a programming language for maths. A proof written in Lean is checked line by line by a small, trusted program. If any step does not follow, the proof does not compile. There is no room to wave a hand and say “this is obvious”.

Axiom’s system, which it calls AxiomProver, split the work between dozens of AI agents. Lead agents broke hard arguments into smaller pieces and reviewed what was being proved. Others searched for existing results or wrote the Lean code. Agents claimed tasks through GitHub, the code-sharing site, and posted progress in Slack. The company says the agents used “a changing mix of models” and does not name them. Human mathematicians handled the hardest problems and engineers kept the system running.

Want AI to save you hours a week? Our free playbook shows you how.Get the free guide →

It did not start from zero. The work builds on Mathlib, a large shared library of maths in Lean written by hundreds of volunteers, and reuses about 1.2 million lines from an earlier open project, Qiuzhen-CFSG, Axiom says.

The blog is unusually frank about what went wrong. Early on, some milestones that looked easy hid huge amounts of unproved groundwork, which the agents had quietly assumed rather than proved. Axiom says it deleted tens of thousands of lines built on those assumptions and started parts again. On 13 October only one milestone closed in a whole day, so the team made the agents re-plan the remaining work into smaller, precisely stated pieces. The agents also wrote proofs faster than Lean could check them, so engineers built a system to share checking work across machines.

What the machines found

The most interesting result is not the size. It is the mistakes. Most of what the agents flagged was minor: typos, errors in tables, or conditions an author forgot to state. But Axiom counts 34 “noteworthy deviations from the published record” that had to be fixed.

One example came from a lemma in the 2004 volumes that said two numbers were always equal. The agents found a case, built from a small group called SL₂(5), where one number was 1 and the other was 2. The lemma had to be weakened, and later arguments that relied on it had to be reworked.

The biggest problem sat in a 1986 argument by John Walter for a key step known as the Unbalanced Group Theorem. The agents found counterexamples to one claim it relied on. The theorem itself survives, because other routes to it exist. But to stay faithful to the original proof, Axiom needed a new argument. With advice from Richard Lyons and Ronald Solomon, two group theorists who worked on the original classification, AxiomProver produced one. The company has written it up in a separate paper and says it is a new result in group theory.

What has not been checked yet

There are real limits here, and Axiom names some of them itself. Lean checks that every step follows. It does not check that the final statement means what mathematicians think it means. That still needs human eyes, and Axiom’s blog says so directly.

Nobody outside the company has yet published an independent rebuild of the proof. That is not a small job. The repository notes say Axiom needed unreleased changes to Lean’s build tools just to get the full check under 24 hours. The detailed list of errors in the literature has also not been published in full; Axiom says it will release it with an advisory board of group theorists. And the top-level statement of the theorem was not written by Axiom but taken from another open project, TauCeti, which is a sensible way to avoid marking your own homework.

Why it matters beyond maths

For most readers, finite simple groups will never come up. The method matters more. Chatbots are famous for sounding right while being wrong, and DailyAI has reported before on language models failing simple logic puzzles. This project points to a different pattern. When AI’s work is checked by a strict, unforgiving program, mistakes get caught instead of hidden, and far more of the work can safely be handed to AI.

The same idea applies to software, chip designs and financial systems, where code can be tested against precise rules. Maths and computer science are also where AI labs are now claiming new results. Earlier this week, DailyAI covered how OpenAI and Anthropic both said AI had broken a long-standing computer science rule.

The catch is the one Axiom’s own agents kept running into. A checker only confirms that the work answers the question it was given. Someone still has to make sure it was the right question. For the enormous theorem, that job now falls to the group theorists.