Lean 形式化有限单群分类定理

HomeProof mapPapersErrataGitHub

Overview Map Agents

Graph

Agent Blueprint Lean Repo

Corpus wheel Treemap Plan Milestones Papers Milestones

By milestone By paper

Steps

Height

Lean lines Commits Statements

Colour

Stone Source work Kind Plan vs Lean

Highlights What's left?

Papers

Mathematics that came out of the formalization. More papers will appear here.

The Unbalanced Group Theorem

Hexagon 2610.00575 · 35 pages

A new group theory result that came out of this formalization project is reported in this paper. While formalizing the first-generation proof, we found counterexamples to a closure assertion used in a published route to the Unbalanced Group Theorem. The paper explains the obstruction and gives an alternative argument for the simple-group case, built on Solomon’s 1976 theory of maximal 2-components, whose key step is Theorem 2.3, the preservation of simple tops.

Read on Hexagon

Errata

We are working with group theorists to compile the errata we found in the literature, and will publish them here.

Zoom in to read each statement

The Classification of Finite Simple Groups, formalized in Lean

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

Explore the proof mapView the formalizationCite

Core contributors Dean Cureton*†, Vasily Ilin†, Bhavik Mehta*†, Niels Voss†

Other contributors 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†, 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}} }

Copy BibTeX

By what they need By when verified

43.1Mlines of Lean

0milestones

0statements

Theorem (classification of finite simple groups). Every finite simple group is a cyclic group of prime order, an alternating group on five or more points, a group of Lie type, or one of the 26 sporadic groups.

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

Milestones People Papers

A lemma or definition is a single result. Nothing sits inside it.

The corpus 0 source works cited by the nodes

1870 1950 1970 1990 2026

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

Milestones 108 Lean lines

43.1Mlines of Lean

100milestones

2.05Mdeclarations

Theorem (classification of finite simple groups). Every finite simple group is a cyclic group of prime order, an alternating group on five or more points, a group of Lie type, or one of the 26 sporadic groups.

This is the Lean Repo, the Lean code as it is organised in the repository. For the agents' starting plan, see the Agent Blueprint

Milestones

The theorem and its case division 5Component type or characteristic 2 type223K lines of LeanTrivial odd cores of involution centralizers (no strong embedding)223K lines of LeanCharacteristic 2 involution centralizers imply characteristic 2 type1K lines of LeanInvolution centralizers modulo their odd core have characteristic 21K lines of LeanA nonabelian group on the list is alternating, of Lie type or sporadic557 lines of Lean

Tools 18Gorenstein–Walter L-balance theorem4.0M lines of LeanGoldschmidt's strongly closed abelian 2-subgroup theorem2.3M lines of LeanSignalizer Functor Theorem (Glauberman, McBride)2.0M lines of LeanAschbacher's Proper 2-Generated Core Theorem1.8M lines of LeanMcBride's Theorem A (signalizer completeness)1.3M lines of LeanLocal C(G,T) theorem (Bender–Hunt–Stellmacher)1.1M lines of LeanBender–Suzuki theorem on strongly embedded subgroups919K lines of LeanMacWilliams's four-generator theorem for 2-groups51K lines of LeanGlauberman's solvable signalizer functor theorem, rank one39K lines of LeanAschbacher's Local C(G,T) / unique maximal 2-local theorem37K lines of LeanGlauberman's Z theorem26K lines of LeanSolvable Signalizer Functor Theorem for elementary abelian 2-groups24K lines of LeanHering's theorem on transitive linear groups13K lines of LeanStrongly embedded Borel subgroup of PSL(2,2 f)9K lines of LeanThompson's transfer lemma (index-2 subgroup)519 lines of LeanThompson's critical subgroup theorem501 lines of LeanZsigmondy's theorem239 lines of LeanGaschütz's splitting theorem179 lines of Lean

Odd order and small 2-rank 12Gorenstein–Harada Sectional 2-Rank 4 Theorem9.0M lines of LeanClassification of simple groups of 2-rank at most 21.9M lines of LeanClassification of simple groups of 2-rank two1.9M lines of LeanAlperin–Brauer–Gorenstein theorem (wreathed Sylow 2-subgroups)1.9M lines of LeanAlperin–Brauer–Gorenstein theorem (semidihedral Sylow 2-subgroups)1.7M lines of LeanWalter's theorem on abelian Sylow 2-subgroups1.6M lines of LeanAschbacher's Theorem 1 (wreathed Sylow 2-subgroups)1.4M lines of LeanGorenstein–Walter theorem (dihedral Sylow 2-subgroups, simple case)976K lines of LeanBender's theorem on abelian Sylow 2-subgroups of rank ≥ 3875K lines of LeanFeit–Thompson theorem188K lines of LeanEven-order nonabelian simple groups have 2-rank at least 219K lines of LeanBrauer–Suzuki theorem19K lines of Lean

Component type 17Classification of K-proper groups of component typeHeads this branch of the proof, 16.1M lines of LeanStandard component case of the component-type analysis16.1M lines of LeanRecognition of groups with an odd-type standard component16.1M lines of LeanLocal B-property for K-proper groups of component type12.4M lines of LeanUnbalanced K-proper simple groups are odd Lie type or alternating12.4M lines of LeanAschbacher's Classical Involution Theorem10.5M lines of LeanClassical involution recognition for a quaternion component10.4M lines of LeanEven standard components: reduction to 32 quotient types4.8M lines of LeanAschbacher–Seitz standard component recognition4.2M lines of LeanSeitz's reduction for centerless even standard components4.2M lines of LeanAschbacher's Embedding Theorems 4.4 and 5.1 for K-groups3.7M lines of LeanStandard component or quaternion component in involution centralizers3.0M lines of LeanSolomon's theorem on Â_n-components2.7M lines of LeanSeitz's theorem on standard components L3(4)2.5M lines of LeanAschbacher's Theorem 5 (permuted semisimple sections)2.4M lines of LeanHolt's Theorem 1 on (*)-groups1.5M lines of LeanAschbacher's tightly embedded subgroups theorem935K lines of Lean

Quasithin groups 9Aschbacher–Smith classification of quasithin groupsHeads this branch of the proof, 9.5M lines of LeanQuasithin groups with a faithful local C-component8.8M lines of LeanQuasithin case H13 with a maximal local subgroup8.8M lines of LeanQuasithin groups without a faithful local C-component4.9M lines of LeanQuasithin groups with a unique maximal 2-local over a Sylow2.7M lines of LeanAschbacher–Smith: groups of type Ru are Rudvalis1.5M lines of LeanStrongly closed TI 2-subgroups force a Bender group1.4M lines of LeanGroups of type HS are the Higman–Sims group1.1M lines of LeanAschbacher–Smith Theorem C (strongly quasithin simple K-groups)28K lines of Lean

Characteristic 2 type, e(G) ≥ 3 20Classification of characteristic 2 type, e(G) ≥ 4Heads this branch of the proof, 24.4M lines of LeanClassification of characteristic 2 type, e(G) = 3Heads this branch of the proof, 22.1M lines of LeanCharacteristic 2 type with e(G) = 3: excluding the local core case21.6M lines of LeanA non-local weak core exists (e(G) ≥ 4)18.5M lines of LeanAschbacher's Uniqueness Case Theorem (e(G) = 3)18.4M lines of LeanGorenstein–Lyons Theorem C (e(G) = 3)18.1M lines of LeanAschbacher's exclusion of the uniqueness case (e(G) ≥ 4)17.8M lines of LeanCharacteristic 2 type with e(G) = 3, attained at the prime 316.9M lines of LeanGorenstein–Lyons Theorem C (e(G) ≥ 4)13.1M lines of LeanAschbacher–Gorenstein–Lyons Embedding Theorem D2 (e(G) ≥ 4)12.5M lines of LeanAschbacher–Gorenstein–Lyons Embedding Theorem D1 (e(G) ≥ 4)12.3M lines of LeanCharacteristic 2 type with e(G) = 3: known group or local core12.1M lines of LeanGF(2)-type recognition (e(G) ≥ 4)10.0M lines of LeanStandard-type recognition (e(G) ≥ 4)9.5M lines of LeanTrichotomy for e(G) ≥ 4: preuniqueness, GF(2) or standard type8.4M lines of LeanGorenstein–Lyons Theorem A (e(G) ≥ 4)7.2M lines of LeanTimmesfeld's large extraspecial 2-subgroup theorem3.5M lines of LeanAschbacher's GF(2)-type theorem2.4M lines of LeanEven Type Theorem (Aschbacher–Lyons–Smith–Solomon)1.5M lines of LeanBounds on odd local ranks167 lines of Lean

Groups of Lie type 5Curtis–Tits presentation theorem (BN-rank at least 3)53K lines of LeanSchur multipliers of PSL(n,q) (Steinberg–Griess)21K lines of LeanDickson's list of subgroups of PSL(2,q)15K lines of LeanBorel–Tits theorem11K lines of LeanTits' classification of subgroups containing a Borel subgroup2K lines of Lean

Sporadic and alternating groups 14Recognition of HN by (2·HS):2 centralizer9.3M lines of LeanYoshida's characterization of Co₃ (centralizer Z₂ × M₁₂)3.3M lines of LeanGriess–Meierfrankenfeld–Segev uniqueness of the Monster3.0M lines of LeanOrder of the Monster's Y₄₄₃ presentation group2.9M lines of LeanSimplicity of the Monster (Y₄₄₃ construction)2.9M lines of LeanExistence of the Monster (Griess–Conway)2.9M lines of LeanBaby Monster recognition from a {3,4}-transposition centralizer2.7M lines of LeanParrott's characterization of the Thompson group Th1.5M lines of LeanParrott's characterization of Fi24' from 2·Fi221.2M lines of LeanJanko–Wong characterization of McL (centralizer 2·A₈)1.0M lines of LeanFischer's theorem on 3-transposition groups337K lines of LeanExistence and uniqueness of Fi22, Fi23 and Fi2490K lines of LeanSimplicity of the Thompson group Th (248-dimensional construction)40K lines of LeanAutomorphisms of A n come from S n (n ≠ 6)499 lines of Lean

Working Just verified one Idle

Just verified

In progress

Messages

Live

Right now

Loading…

CFSG Milestone Proposition Lemma Definition

Milestone Theorem Definition Structure, class or instance Certificate

+−◎

▶ Grow the tree⟳ Turn

Back to the map

▶ Replay

Now Oct 27, 4:35 PM

0 / 0 milestones, 0 statements under complete milestones

1×4×16×