Axiom, a startup building AI systems for mathematics, said it has produced a complete computer-checked proof of the Classification of Finite Simple Groups in the Lean proof assistant. The company described the work in a research post dated October 26, 2026, and announced it publicly on October 27. According to Axiom, the project took 24 days and produced about 43.1 million lines of Lean code. (Axiom (opens in a new tab); TokenPost (opens in a new tab); Unite.AI (opens in a new tab))
The classification is one of the longest results in mathematics. It lists every finite simple group, the basic building blocks from which all finite groups are assembled: cyclic groups of prime order, alternating groups, sixteen infinite families of groups of Lie type, and 26 sporadic groups. The human proof spans roughly 15,000 pages across more than 500 articles written by about 100 mathematicians over several decades. (Axiom (opens in a new tab); TokenPost (opens in a new tab))
How the agents did the work
Axiom said dozens of AI agents worked from a shared map of the published literature that split the proof into 108 milestones and about 380 smaller tasks. Lead agents broke arguments into pieces and reviewed statements, while other agents claimed milestones and reported progress. Human mathematicians at the company investigated the most consequential problems the agents raised. (Axiom (opens in a new tab); Unite.AI (opens in a new tab))
The process was not smooth. Axiom said early work relied on unproven assumptions, and the team deleted tens of thousands of lines and replanned on October 13, a day when only one milestone closed. The company said its agents proved that the Monster, the largest sporadic group, is simple on October 10. Axiom also said about 1.2 million lines came from an earlier project called Qiuzhen-CFSG. (Axiom (opens in a new tab); Unite.AI (opens in a new tab))
Errors found in the published record
According to Axiom, the formalization found 34 noteworthy deviations from the published record, along with typos, table errors and dropped hypotheses. The agents found counterexamples to a step in John Walter's 1986 memoir on the Unbalanced Group Theorem, which Axiom replaced with a new argument. A lemma in the Aschbacher and Smith volumes on quasithin groups was also corrected. The company said these issues did not overturn the classification itself. (Axiom (opens in a new tab); RuntimeWire (opens in a new tab); Unite.AI (opens in a new tab))
Axiom said it formalized the first-generation proof rather than the second-generation proof, which is still incomplete. Group theorists Richard Lyons and Ronald Solomon were consulted on the arguments and serve as advisors. TokenPost noted that a machine check confirms the encoded steps follow from the encoded assumptions, but people still need to confirm that the formal statement matches the intended theorem. (Axiom (opens in a new tab); TokenPost (opens in a new tab))
The result has not yet been reproduced outside the company. Asked by RuntimeWire whether any outside party had independently built and checked the proof, Axiom founder and CEO Carina Hong answered that it had not happened yet, and said the company is publishing its build artifacts to encourage others to do it. (RuntimeWire (opens in a new tab))
In NeuraFeed's reading, the size of the project matters as much as the theorem. A proof this long has long been considered too large for any single person to check in full, and Axiom's claim is that AI agents can now do the bulk of the translation into machine-checkable form while humans focus on the hardest judgment calls. The claim rests on the company's own account until outside groups rebuild the code.
