Math AI company Axiom has announced that its AxiomProver agent swarm completed a Lean formalization of the Classification of Finite Simple Groups (CFSG) in 24 days, calling it the first complete computer-checked proof of the theorem. The code is open-sourced on GitHub under the Apache-2.0 license. The repository states that the final version contains no sorry placeholders, does not use native_decide, and relies only on three standard axioms: propositional extensionality, classical choice and quotient soundness.
The classification is often described as the "periodic table of symmetry." It says every finite simple group is either a member of one of 18 infinite families or one of 26 sporadic groups. The original proof is spread across more than 500 papers and roughly 15,000 pages, written by about 100 mathematicians from around 1955 to 2004. The last piece, the quasithin case by Aschbacher and Smith, runs to 1,221 pages on its own.
What happened in those 24 days
According to Axiom's account, the project set up a Slack workspace for coordination on October 1, and the first agents came online on October 2. The proof was broken into 108 milestones and about 380 smaller tasks. Agents claimed tasks through GitHub issues and reported progress in Slack. A lead agent split up the work and reviewed statements, while the other agents either searched for existing results or wrote Lean proofs, delegating further down when a prerequisite was missing.
It was not a smooth run. An early batch of code was deleted wholesale after a hidden assumption turned out to be wrong, and the team had to replan. Build speed later became the bottleneck; engineers used caching and parallel checking and moved finite computations out into verifiable certificates, bringing a full build to under 24 hours. On October 10, the project separately announced a proof that the Monster group is simple.
On the source side, Axiom says it ingested 715 papers and books in total, and reused about 1.2 million lines of code from the earlier Qiuzhen-CFSG project, along with existing formal libraries such as Mathlib and Tau Ceti.
Errors caught along the way
During formalization, the team logged 34 notable mathematical discrepancies. The one drawing the most attention sits on the route through the Unbalanced Group Theorem (UGT): a closure claim in Walter's 1986 memoir has a counterexample, in which starting from PSL₂(49) leads to PSL₂(7), a group the family explicitly excludes. A lemma by Aschbacher and Smith also turned out to have an SL₂(5) counterexample; once the equality is changed to an inequality, the arguments that follow have to be extended.
Axiom published a separate 35-page paper proposing a replacement argument, and worked with advisers including Lyons and Solomon to patch this route. The company repeatedly stresses that these counterexamples do not overturn the UGT itself, let alone shake the classification theorem.
"the classification remains the achievement of the mathematicians who discovered the groups"
Compared with earlier machine verification
The comparison most often drawn is with the verification of the Odd Order Theorem that Gonthier's team completed in Coq in 2012. That theorem comes from Feit and Thompson's 255-page paper of 1963; the project took about six years and is one cornerstone of the classification proof. Axiom's effort covers the whole building, and it was counted in days.
The two cannot be compared directly on speed. The Odd Order project built its libraries almost from scratch, whereas Axiom stood on top of Mathlib and the earlier 1.2 million lines of CFSG code, and used "dozens" of agents. The compute, hardware and total cost behind the run were not disclosed, and neither were the human hours. The 24 days is the duration of the formalization project itself; it does not include the decades of human work it depends on.
Several caveats are also stated openly. The project metadata labels the review as a "self-assessment," and no third party has yet reproduced the full build from a clean environment. Machine checking only guarantees that the derivations follow from the assumptions as written; whether the definitions in the classification statement faithfully match the original theorem still needs to be checked line by line by group theorists. The UGT paper was posted on a preprint platform without peer review, and Axiom says an errata list will be hosted on the project page.
For people working in formalization, there are two things to watch next: whether the community can independently run all 43.1 million lines, and how many of the 34 discrepancies the original authors' side will confirm.
Sources: Axiom project announcement and GitHub repository, Unite.AI, CocoLoop, Kingy AI. Lean line counts, declaration counts, milestone counts and discrepancy counts follow the figures published by Axiom; the Odd Order Theorem verification timeline is based on Microsoft Research materials.