Axiom Math, a startup building AI systems for mathematics, says it has turned one of the longest proofs ever written into code a computer can verify line by line. In a post dated October 26 and a public GitHub repository announced on October 27, the company released a Lean 4 formalization of CFSG, the classification theorem for finite simple groups often called the enormous theorem, and credited most of the work to swarms of its AxiomProver agents directed by engineers and mathematicians.
The classification says every finite simple group falls into one of four kinds: cyclic groups of prime order, alternating groups, groups from the Lie-type families, or the 26 sporadic exceptions, of which the Monster is the biggest. These groups act as the building blocks of all finite groups. The human proof runs to about 15,000 pages spread over upwards of 500 papers from roughly 100 mathematicians, was declared complete in 1983, and needed further work until a 1,221-page treatment of the quasithin case appeared in 2004.
Axiom says the project ran for 24 days. It opened a coordination channel on October 1, built a proof map from the literature with 108 milestones and about 380 tasks, and let agents claim work, delegate missing prerequisites and push results into a shared repository. Lead agents broke down hard arguments and reviewed statements while others searched for existing results and wrote Lean. The output came to about 43.1 million lines and, per the project site, 2.05 million declarations. Axiom did not say which AI models the agents ran on.
According to the README, the development is sorry-free, targets Lean v4.35.0-rc3, builds on Mathlib and the TauCeti project, whose statement of the classification it uses, and depends only on the standard axioms, with no native_decide. Roughly 1.2 million of its lines are taken from the earlier Qiuzhen-CFSG effort. A full build took Axiom close to a day even with unreleased changes to the Lake build tool. The code is licensed Apache 2.0.
The most interesting outcome may be what the agents found along the way. Axiom reports 34 noteworthy deviations from the published record, mostly small errors but including counterexamples to a closure step in John Walter's 1986 route to the Unbalanced Group Theorem. The company stresses the theorem itself is not in doubt. To bridge the gap, AxiomProver proved a new preservation result built on Ronald Solomon's 1976 theory of maximal 2-components, described in an accompanying paper; Axiom mathematicians later found a shorter argument. Group theorists Richard Lyons and Ronald Solomon advised the project and will help curate an errata list that has not yet been released.
For comparison, the 255-page Feit-Thompson odd order theorem, one ingredient of the classification, took a team led by Georges Gonthier six years to formalize in Coq, finishing in 2012. Axiom's blog presents the new work as building on that tradition and on Mathlib rather than replacing the mathematicians who produced the original proof.
Independent observers urge caution. Neural Brew, reporting on October 27, said no complete independent review had been published and that it could not confirm the proof recompiles. Arncof's Yoseph Franco found no outside rebuild or statement from Lean or Mathlib maintainers, noted that Axiom's own X thread cited 50 million lines and hundreds of errata against the blog's 43.1 million and 34, and pointed out that many enthusiastic posts came from people tied to the company. Lean checks every deduction, but humans still have to confirm that the formal statement captures the classification, a review Axiom itself has asked group theorists and the Lean community to carry out.