Axiom Math Releases Complete Lean Proof of the Classification of Finite Simple Groups

Axiom Math said on October 27 that it is releasing what it calls the first complete computer-checked proof of the Classification of Finite Simple Groups. The formal development is published in a public GitHub repository and runs to about 43.1 million lines of Lean code. Axiom describes a 24-day effort carried out by its own team. The classification is one of the largest results in modern algebra, assembled from decades of papers by many authors. A machine-checked version gives the field a single artifact that a proof assistant can verify line by line, instead of relying on the consensus of human referees. Earlier this week OpenAI also announced AI-generated results in mathematics and physics, though those claims still face peer review. For teams building coding agents, the project is a large test of long-horizon work checked by a strict verifier rather than by reading diffs. The lesson is to pair generation with a formal or automated checker that can reject bad output at scale.