AI agents just put math's longest proof into Lean. They left 34 notes.

The longest proof humans ever wrote just went through something every programmer knows: code review.

What happened. Axiom, an AI math startup, says it has released the first complete computer-checked proof of the Classification of Finite Simple Groups, often called "the enormous theorem." The original proof runs to roughly 15,000 pages across more than 500 articles by about 100 mathematicians, written over decades. Axiom's engineers and mathematicians directed swarms of dozens of AI agents for 24 days, producing about 43.1 million lines of code in the Lean proof assistant, where a small program (Lean's kernel) checks every logical step. Axiom posted the news on X on the morning of October 27; its blog post is dated October 26.

What the theorem says. Finite simple groups are the "atoms" of symmetry. The classification says every one is either a cyclic group of prime order, an alternating group, one of 16 families of groups of Lie type, or one of exactly 26 "sporadic" oddballs, the largest being the Monster, with roughly 8 x 10^53 elements.

The review comments. According to Axiom:

• Most problems the agents flagged in the published papers were minor: typos, errors in tables, dropped hypotheses.
• 34 were "noteworthy deviations from the published record" that had to be resolved. Axiom says it will publish the full errata list.
• The biggest involved the Unbalanced Group Theorem: the agents found counterexamples to a step in a 1986 published argument. The theorem itself still holds; the agents and Axiom's team had to route around the broken step, which produced a new result in group theory, written up in a separate paper.
• Early on, agents "assumed rather than proved" some big prerequisites, and Axiom deleted tens of thousands of lines and restarted parts of the work.

Who did what. This was not agents alone. Axiom's mathematicians investigated the hardest problems, and group theorists who worked on the original classification, including Richard Lyons and Ronald Solomon, were consulted. The project also builds on Lean's Mathlib library and about 1.2 million lines from the earlier Qiuzhen-CFSG project. MODEL has not checked the proof ourselves; the code is public for anyone who wants to.

Our take. Calling this "AI solved math" would be wrong; the math was finished decades ago. What's new is the review. Humans wrote a proof too long for any one person to fully check, and machines, steered by people, went line by line and found where it didn't quite say what everyone thought it said. That's the kind of AI work worth getting excited about.