Axiom Used Swarms of AI Agents to Formalize the Classification of Finite Simple Groups in Lean in 24 Days: About 43.1 Million Lines of Code, and 34 Noteworthy Deviations Found in the Published Proof

The "enormous theorem," checked by machine

The Classification of Finite Simple Groups (CFSG) says every finite simple group is cyclic of prime order, alternating, one of 16 infinite families of groups of Lie type, or one of 26 sporadic groups. It is often called the longest proof in mathematics: the original runs to roughly 15,000 pages across more than 500 articles by about 100 mathematicians over several decades. Its completion was announced in 1983, but a gap involving quasithin groups wasn't closed until 2004.

Math AI company Axiom Math announced on October 27 that it had completed a full formalization of CFSG in the Lean proof assistant, with every logical step checked by Lean's kernel. According to the company, engineers and mathematicians directed swarms of dozens of AI agents over 24 days, counting from the Slack coordination channel opened on October 1 and the first agents going live on October 2, producing about 43.1 million lines of Lean. The code and an interactive proof map are public on GitHub (AxiomMath/CFSG) and the project site.

Organizing dozens of agents

Building on existing Lean work and a proof map assembled from the literature, the team split the project into 108 milestones and about 380 smaller tasks. Agents claimed tasks through GitHub issues, delegated not-yet-formalized prerequisites to other agents, and merged results into a shared repository. Lead agents broke down hard arguments and reviewed the statements being formalized, human mathematicians handled mathematical obstructions, and engineers kept the system productive.

It didn't go smoothly. Some milestones that looked manageable early on hid enormous prerequisites that agents had simply assumed; the team deleted tens of thousands of lines built on those assumptions and restarted. At one point agents produced proofs faster than Lean could recheck them, so engineers built a build cache shared across machines and moved expensive finite computations into separately checkable certificates. On October 13 only one milestone closed, prompting a dedicated replanning round that split unfinished milestones into smaller, precisely stated theorems. Because the second-generation proof (the multi-volume work by Gorenstein, Lyons, Solomon and others) is still not complete, Axiom formalized the first-generation proof.

What turned up

Formalization forces every detail a human reader would fill in to be written out, which exposed problems in the published proofs. Most were typos, table errors or dropped hypotheses, but there were 34 noteworthy deviations. One example comes from Aschbacher and Smith's quasithin volumes: a lemma asserted two quantities were equal, and agents found a counterexample using the group SL₂(5) in which one was 1 where equality required 2. Replacing the equality with an inequality meant later arguments that relied on it needed separate handling.

The most significant involved the Unbalanced Group Theorem (UGT). Agents found counterexamples to a closure assertion in John Walter's 1986 argument, leaving a key inference unjustified without refuting UGT's conclusion. After consulting group theorists who worked on CFSG, including Richard Lyons and Ronald Solomon, the team took a different route based on Solomon's 1976 theory of maximal 2-components, in which AxiomProver proved and formalized a new group theory result, the "preservation of simple tops." Axiom says it will compile and publish an errata list together with group theorists.

Note that these errata and repairs come from the Axiom team so far and still await independent review by group theorists. Formal verification checks the deductions behind the theorem statement in Lean; whether that statement accurately expresses CFSG is still a question for human review.