The makers of AxiomProver have shared the digital translation of the Classification of Finite Simple Groups on GitHub, enabling researchers to validate every logical step of the proof through code. During the formalization process, the startup’s AI agents identified 34 discrepancies in the published work, including errors in a 1986 argument for the Unbalanced Group Theorem. To fix the flaw, the system developed an alternative proof based on research from 1976, which allowed the underlying theorem to remain intact while correcting the historical record.

The project utilized a swarm of AI agents to convert roughly 15,000 pages of text authored by more than 100 mathematicians into 43 million lines of Lean code. The $1.6B startup completed the translation in 24 days, a task that involved dividing the work into 380 separate segments and checking the results of 715 different papers and books. The result is the largest computer-verified proof in history, eliminating the need for a human to manually read the entire interconnected body of work to verify its accuracy.