Formalizing the Classification of Finite Simple Groups (CFSG) within Lean

The Classification of Finite Simple Groups stands as a monumental pillar of modern mathematics, representing a massive collaborative effort. The original "first-generation" proof is an immense undertaking, spanning thousands of pages across various journals and authored by approximately one hundred mathematicians over several decades.

Essentially, the CFSG establishes that any finite simple group must fall into one of the following categories:

• Cyclic groups of prime order ($\mathbb{Z}_p$)
• Alternating groups ($A_n$ for $n \ge 5$)
• Groups of Lie type
• One of the 26 sporadic groups

The Lean Formalization Project

A comprehensive formalization of this proof has now been achieved using the Lean theorem prover. This means every single logical transition in the first-generation proof has been rigorously verified by the Lean kernel.

Project Metrics at a Glance

Project Architecture

The workflow of the formalization can be visualized as follows:

The Unbalanced Group Theorem: A New Discovery

One of the most significant outcomes of this formalization process was the discovery of a mathematical error in existing literature. While translating the first-generation proof, the team encountered a problem regarding the Unbalanced Group Theorem.

Specifically, they found that a closure assertion used in a previously published route to the theorem was incorrect. After identifying counterexamples to this assertion, the team developed an alternative logical path for the simple-group case.

The Solution: The team utilized Solomon’s 1976 theory regarding maximal 2-components. The pivotal element of this correction is Theorem 2.3, which focuses on the preservation of simple tops.

This finding is detailed in the paper Hexagon 2610.00575 (spanning 35 pages).

Project Resources & Contribution

The project is not just a codebase but a living ecosystem of mathematical verification.

Available Assets

• Lean Repo: The primary source code for the formalization.
• Agent Blueprint: The initial instructional framework provided to the agents.
• Proof Map: An interactive visualization (Treemap/Graph) allowing users to explore milestones, statements, and Lean status.
• Errata List: A collaborative effort with group theorists to document errors found in the original literature.

The Team

Core Contributors:

• Dean Cureton
• Vasily Ilin
• Bhavik Mehta
• Niels Voss

Additional Contributors: The project involved a wide array of mathematical and engineering talent, including Rafael Cabral, Colin Defant, Erik Gregory, Aaron Hill, Letong Hong, Qinheping Hu, Dustin Jamner, Albert Jiang, Tadeusz Jordan, Andranik Kurghinyan, Kenny Lau, Jonathan Laurent, David Liang, Jannis Limperg, Simon Mahns, Brian Nugent, Connor Olson, Ken Ono, Eric Paul, Dhruv Rajan, Karun Ram, Charlie Ray, Ho Chung Siu, Ashvin A. Swaminathan, Jesse Thorner, Aleksey Tsaplin, and Chenkai Wang.

Citation

To cite this monumental work, use the following BibTeX entry:

@misc{axiom-cfsg, 
  author = {Cureton, Dean and Ilin, Vasily and Mehta, Bhavik and Voss, Niels and Cabral, Rafael and Defant, Colin and Gregory, Erik and Hill, Aaron and Hong, Letong and Hu, Qinheping and Jamner, Dustin and Jiang, Albert and Jordan, Tadeusz and Kurghinyan, Andranik and Lau, Kenny and Laurent, Jonathan and Liang, David and Limperg, Jannis and Mahns, Simon and Nugent, Brian and Olson, Connor and Ono, Ken and Paul, Eric and Rajan, Dhruv and Ram, Karun and Ray, Charlie and Siu, Ho Chung and Swaminathan, Ashvin A. and Thorner, Jesse and Tsaplin, Aleksey and Wang, Chenkai}, 
  title = {Lean formalization of the classification of finite simple groups}, 
  year = {2026}, 
  howpublished = {\url{https://github.com/AxiomMath/CFSG}}, 
  note = {Interactive proof map at \url{https://cfsg.axiommath.ai}} 
}