Axiom says AI agent swarms formalized the 15,000-page classification of finite simple groups in Lean in 24 days

The Classification of Finite Simple Groups (CFSG) lists the basic building blocks of every finite group. Its original proof is often called the longest ever written by humans: roughly 15,000 pages, in more than 500 articles, by about 100 mathematicians. Axiom Math now says it has the first complete computer-checked proof of it, written in the Lean proof assistant.

How it was built

In Axiom’s words: “Over 24 days, engineers and mathematicians at Axiom Math directed swarms of dozens of AI agents in a project that produced approximately 43.1 million lines of code” in Lean. The first swarm went live on 2 October. Agents claimed milestones through GitHub issues, and the team built a system to share cached build results between workers because agents were producing proofs faster than Lean could recheck them.

The proof builds on Mathlib and incorporates about 1.2 million lines from the existing Qiuzhen-CFSG project. Axiom thanks three outside advisors, the group theorists Richard Lyons, Ron Solomon and Dan Nakano.

What the agents found in the old proof

Translating the literature into Lean surfaced problems. Most were minor, such as typos, table errors or dropped hypotheses. But Axiom reports “34 noteworthy deviations from the published record that needed to be resolved”. The main one is in the Unbalanced Group Theorem, where Axiom gives a counterexample, built with PSL2(49), to a closure assertion in a 1986 paper by John Walter. Axiom says its prover, AxiomProver, proved a new result to close that gap, and the details are on the errata and proof-map site.

Can you check it?

That is the point of a formal proof, and the code is public. The CFSG repository is Apache-2.0. Its README says the proof is “sorry-free” (no unfinished steps), uses only Lean’s standard axioms, avoids native_decide, and takes its theorem statement from the TauCeti project. A full lake build takes under 24 hours and currently needs Lake changes that are not merged upstream.

So the claim is checkable, but it is fresh: the repository appeared on 27 October and no independent group has reported rebuilding it yet. For the wider story of Lean in research maths, see our posts on Lean-verified journal proofs and the Navier-Stokes formalization.