Axiom's agent swarm formalized the Enormous Theorem and found 34 places the textbooks were off
The Classification of Finite Simple Groups is the theorem mathematicians call enormous for a reason: its proof is spread across hundreds of papers and tens of thousands of pages, written over half a century. Axiom just published a complete Lean formalization of it, and most of the work was done by an agent swarm in about three and a half weeks.
The numbers on the project site: 43.1 million lines of Lean, 2.05 million declarations, 715 papers and books covered. The first swarm went live on October 2. Agents claimed milestones through GitHub issues, lead agents broke hard arguments into pieces and reviewed the statements being formalized, and Lean checked every deduction. On October 10 the team posted "WE PROVED MONSTER IS SIMPLE." The public repo went up on October 27. Group theorists Lyons and Solomon were consulted along the way.
The part that matters most is not the size. The swarm surfaced 34 noteworthy deviations from the published record, including a counterexample to a lemma in Aschbacher and Smith and problems with a closure assertion in the proof of the Unbalanced Group Theorem. Literature that humans had checked for decades still had holes, and agents working under a strict checker found them.
The honest part is just as useful. Axiom says agents sometimes "had assumed rather than proved" prerequisites, and the team "deleted tens of thousands of lines built on those assumptions." Agents also produced proofs faster than Lean could recheck them. So the lesson is the same one we keep seeing this month: the swarm supplies volume, the verifier supplies truth, and the human job shrinks to checking that the top-level statement and its definitions say what you meant.
Project: https://cfsg.axiommath.ai/ Blog: https://axiommath.ai/research/the-enormous-theorem-formalized/ Repo: https://github.com/AxiomMath/CFSG
← Back to all articles
The numbers on the project site: 43.1 million lines of Lean, 2.05 million declarations, 715 papers and books covered. The first swarm went live on October 2. Agents claimed milestones through GitHub issues, lead agents broke hard arguments into pieces and reviewed the statements being formalized, and Lean checked every deduction. On October 10 the team posted "WE PROVED MONSTER IS SIMPLE." The public repo went up on October 27. Group theorists Lyons and Solomon were consulted along the way.
The part that matters most is not the size. The swarm surfaced 34 noteworthy deviations from the published record, including a counterexample to a lemma in Aschbacher and Smith and problems with a closure assertion in the proof of the Unbalanced Group Theorem. Literature that humans had checked for decades still had holes, and agents working under a strict checker found them.
The honest part is just as useful. Axiom says agents sometimes "had assumed rather than proved" prerequisites, and the team "deleted tens of thousands of lines built on those assumptions." Agents also produced proofs faster than Lean could recheck them. So the lesson is the same one we keep seeing this month: the swarm supplies volume, the verifier supplies truth, and the human job shrinks to checking that the top-level statement and its definitions say what you meant.
Project: https://cfsg.axiommath.ai/ Blog: https://axiommath.ai/research/the-enormous-theorem-formalized/ Repo: https://github.com/AxiomMath/CFSG
Comments