Axiom's AI agents formalize the classification of finite simple groups in Lean

Axiom Math said on 26 October 2026 that it has released the first complete computer-checked proof of the Classification of Finite Simple Groups, written in the Lean proof assistant [1]. Over 24 days, its engineers and mathematicians directed swarms of dozens of AI agents that produced about 43.1 million lines of Lean code [1][2].

What did Axiom formalize?

The classification, often called the enormous theorem, lists the building blocks of all finite groups, the mathematics of symmetry [1]. It says every finite simple group is cyclic of prime order, alternating, of Lie type, or one of 26 sporadic groups [2].

Axiom says the original proof runs to roughly 15,000 pages in more than 500 articles by about 100 mathematicians [1]. Its Lean version follows the first-generation proof and, according to the project's GitHub page, is sorry-free, meaning no step is left unproved [3].

Axiom says its AI agents produced about 43.1 million lines of Lean in 24 days to formalize the classification. The project site lists 2.05 million declarations and 715 papers and books in the corpus [2]. Axiom says the formalization incorporates about 1.2 million lines from an earlier project, Qiuzhen-CFSG, and builds on the Mathlib library [1].

How did the agent swarm work?

Axiom opened a Slack channel for the project on 1 October 2026 and the first swarm went live on 2 October [1]. A proof map drawn from the literature split the work into 108 milestones and about 380 smaller tasks, which agents claimed through GitHub issues [1].

Lead agents broke down hard arguments and reviewed statements, while others searched for existing results or wrote Lean proofs [1]. Human mathematicians handled mathematical obstructions and engineers kept the system running [1]. Axiom says it deleted tens of thousands of lines built on unproved assumptions and restarted parts of the work [1].

On 10 October, according to Axiom, a message in the channel announced that the agents had proved the Monster group is simple [1]. Lean checks the deductions, while humans inspect the final statement and definitions to confirm they express the intended theorem [1].

What errors did the AI agents find?

Axiom says most problems it found were minor, such as typographical errors, mistakes in tables or dropped hypotheses [1]. Axiom found 34 noteworthy deviations from the published record that needed to be resolved. The most substantial case concerned the Unbalanced Group Theorem [1][2].

There, the agents found counterexamples to a closure assertion in John Walter's 1986 argument, which left a key step unjustified without refuting the theorem itself [1]. An alternative argument built on Ronald Solomon's 1976 theory of maximal 2-components became a new result, written up in a 35-page paper [1][2]. Solomon and Richard Lyons, who worked on the original classification, were consulted [1].

Has anyone outside Axiom checked the proof?

Not yet, according to RuntimeWire [4]. Carina Hong, Axiom's CEO, told RuntimeWire that no outside group has yet rebuilt and checked the proof. Axiom is publishing the build artifacts so others can reproduce it [4].

The GitHub page says a single build command checks the whole project, and that Axiom used pending changes to Lake, Lean's build tool, to get the build time under 24 hours [3]. The AI Pin covered OpenAI's separate claims of new math discoveries on 27 October.

Our read

Opinion: Auditing a proof that no single person has ever fully read is a more convincing use of AI in mathematics than chasing new headlines, and finding 34 real deviations shows the audit had teeth. The result is only as strong as its outside checks, though, so an independent rebuild and a group-theory errata review matter more than the line count.

What we could not verify

• Whether the 43.1-million-line proof builds and checks outside Axiom; according to RuntimeWire, no outside group had completed a rebuild as of 27 October 2026.
• Which AI models powered the agents; Axiom only says they used a changing mix of models.
• How independent group theorists judge the result; we found no published reaction from a group theorist outside Axiom's advisory circle at publication.
• The full list of the 34 noteworthy deviations; Axiom says it will publish the errata list after consulting group theorists.
• Whether the new paper on the Unbalanced Group Theorem holds up under peer review; it is posted on Hexagon, and we could not confirm any journal peer review.