AI agents help formalize the Classification of Finite Simple Groups in Lean

A team has published a complete Lean formalization of the first-generation proof of the Classification of Finite Simple Groups, one of the largest collaborative results in mathematics. The original proof runs to thousands of journal pages written by about a hundred mathematicians over several decades, and it says that every finite simple group is cyclic of prime order, alternating, of Lie type, or one of 26 sporadic groups. The formalization comes to 43.1 million lines of Lean and 2.05 million declarations, built from a corpus of 715 papers and books, with every logical step checked by Lean's kernel.

What makes this a Kav News story is how it was done. The project used AI agents working from an initial "Agent Blueprint," so this is machine-checked mathematics produced substantially by machines, though the page is vague about exactly how much the agents wrote. The core work is credited to a small group including Dean Cureton, Vasily Ilin, Bhavik Mehta, and Niels Voss, with Letong Hong as principal investigator.

The formalization did more than confirm known results. While checking the argument, the team found counterexamples to a closure claim used in one published route through the Unbalanced Group Theorem, a real gap in the literature, and wrote a 35-page paper giving an alternative argument based on Solomon's 1976 theory of maximal 2-components. The project site has the full breakdown.

Why it matters

If you follow formal verification or AI for math, this is a concrete data point on scale: agents helped machine-check a proof too large for any person to hold in their head, and in doing so found a flaw humans had missed. That is the case for formalization, made with a result that matters.