James Routley

The classification of finite simple groups is one of the great collective achievements of mathematics. Its first-generation proof spans thousands of journal pages, written by about a hundred mathematicians over several decades. It shows that every finite simple group is cyclic of prime order, alternating, of Lie type, or one of 26 sporadic groups.

Here we present a complete formalization in Lean following the first-generation proof, with every logical step checked by Lean’s kernel. Along the way, we found an issue in a published argument for the Unbalanced Group Theorem. The accompanying paper explains the issue and the alternative route used in our proof. Our blog post tells the full story.

Lines of Lean: 43.1M
Declarations: 2.05M
Milestones: 100
Papers and books: 715

Core contributorsDean Cureton^*^†, Vasily Ilin^†, Bhavik Mehta^*^†, Niels Voss^†

Other contributorsRafael 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^†, Chenkai Wang^†

^*Mathematical contributors^†Engineering contributors^◇Principal investigator

Cite this work

@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}}
}

This is the Agent Blueprint, the initial blueprint we gave the agents. For the Lean code itself, see the Lean Repo

The corpus 139 source works

18701950197019902026

Each block is a paper or book, sized by the statements it supplies. Hover to find its statements.

Classification of Finite Simple Groups Formalized in Lean

Cite this work

The corpus 139 source works

Milestones 108