Axiom Math said on October 26 that it had finished what it describes as the first complete computer-checked proof of the Classification of Finite Simple Groups in Lean.
In the Axiom Math announcement, the company says the project formalized the first-generation CFSG proof and reduced it to steps Lean could verify mechanically. Axiom also says the effort ran for 24 days, used dozens of AI agents, and generated roughly 43.1 million lines of Lean code.
The formalization did more than reproduce the literature. Axiom says it surfaced 34 noteworthy departures from published arguments, and it flagged a problem in a published route to the Unbalanced Group Theorem. The company says it plans to publish a longer errata list for mathematicians.
For builders, the interesting part is less the headline theorem than the operating model: break a dependency-heavy problem into tracked subproblems, then keep a verifier in the loop so plausible output does not get mistaken for a finished result. That pattern is relevant anywhere agents need to prove coverage and correctness, not just produce text that looks complete.