Axiom Math releases 43.1M-line Lean proof of group classification

Axiom Math said on October 27, 2026 it released the first complete computer-checked proof of the Classification of Finite Simple Groups. The Lean formalization spans 43.1 million lines, 2.05 million declarations and 715 sources, produced in 24 days by swarms of AI agents; the team found 34 notable deviations from published proofs.

• 43.1M lines of Lean, 2.05M declarations and 715 sources in the corpus
• The project took 24 days across 108 milestones and about 380 tasks
• 34 notable deviations from published proofs, including an error in the quasithin volumes
• Code is Apache-2.0 licensed and lake build checks the full development in under 24 hours