Axiom Math has produced a machine-checked Lean formalization of the Classification of Finite Simple Groups (CFSG), the longest mathematical proof in history, spanning roughly 15,000 pages across more than 500 articles by approximately 100 mathematicians. The formalization took 24 elapsed days and produced approximately 43.1 million lines of Lean code across 229,089 files, as independently counted by The Hum. Axiom describes this as the first fully computer-checked proof of CFSG. The company published the source code publicly and has invited group theorists and the Lean community to independently validate the formalization by rerunning the proof check.
Line counts vary across sources: Axiom's research page and a detailed blog report state approximately 43.1 million lines, The Hum independently counted 43,068,005 lines, and an Axiom post gives 50 million lines; no source explains the gap. The formalization incorporates approximately 1.2 million lines from the earlier Qiuzhen-CFSG effort and builds on Mathlib. Axiom published random seed scripts so external teams can independently replay verification of lemma subsets on consumer hardware.
The work was done by swarms of dozens of AI agents guided by mathematicians and engineers. AI lead agents decomposed arguments and reviewed statements while other agents searched literature, wrote proofs, or delegated prerequisites, with human mathematicians handling obstructions. Axiom attributes the capability jump to simultaneous improvements across models, the agent harness, and infrastructure, noting that earlier this year a correct 10,000-line Lean proof took weeks, making the CFSG task approximately 4,000 times larger. Custom changes to Lean's Lake build system were required to complete the build within 24 hours.
During the project, the AI found counterexamples to a claim in the published CFSG proof. The overall theorem still holds, and AxiomProver proved a new result to replace the flawed step, drawing on ideas from Ronald Solomon. The formalization surfaced 34 noteworthy departures from published mathematical arguments, including a flagged problem in a published route to the Unbalanced Group Theorem. Axiom plans to publish a longer errata list for the mathematics community.
The proof repository contains no 'sorry' statements and uses only Lean's standard axioms, avoiding native_decide. Axiom describes the review as self-assessed and the formalization has not been independently audited. The repository arrived as a single public commit rather than a reviewable development history. One report characterizes the release as a high-value verification candidate rather than a finished consensus event, with credibility contingent on others reproducing the build and independently validating the target statement. Axiom leads corrected press releases from other AI vendors that implied agents alone proved CFSG, emphasizing human direction and Lean as the ultimate arbiter.