How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The Finite Simple Group Classification Landscape
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Conjugacy in Sₙ, Generation, and the Simplicity of Aₙ
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Cyclic Groups and Direct Products
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Normal Subgroups and Quotient Groups
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Relations, Functions, and Quotients
- Roots, Rational Powers, and Classical Inequalities
- Socles and the Onan Scott Landscape
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Fundamental Theorem of Finite Abelian Groups
- The ZFC Axioms and the Basic Set Constructions
2 · Summary
This orientation page separates the local finite-group argument about components and from the classification and its consequences, which are recorded as sourced external landmarks. Names of Lie-type families follow the cited table; no Lie-algebra construction is supplied.
3 · Logical flowchart
4 · Definitions, theorems and proofs
Simple groups as composition factors
Jordan–Hölder makes composition factors invariant but does not reconstruct extension data.
Quasisimple groups, components, and the layer
Definition
Quasisimple means perfect with simple central quotient; components are subnormal quasisimple subgroups and E(G) is generated by them.
Distinct components commute
Statement
Distinct components of a finite group commute.
Facts & Assumptions
Given: Let and be distinct components of .
Smith's component theorem says that two components of a finite group either coincide or centralize one another.
Proof
Smith's component theorem says that two components of a finite group either coincide or centralize one another. It applies because and are subnormal quasisimple subgroups, exactly the components of Quasisimple groups, components, and the layer.
Since , the second alternative gives ; equivalently, and commute.
The generalized Fitting subgroup
Definition
For finite G, F*(G)=F(G)E(G).
The generalized Fitting subgroup contains its centralizer
Statement
For a finite group , .
Facts & Assumptions
Given: Let be finite and put .
Smith's generalized-Fitting theorem says that contains its centralizer in every finite group .
Proof
Smith's generalized-Fitting theorem states, with these conventions, that the product of the Fitting subgroup and the layer is self-centralizing. Its component input is Distinct components commute, and its finite-group hypotheses are exactly those in the statement.
Therefore , which is .
p-local subgroup
Definition
A p-local subgroup is N_G(P) for a nontrivial p-subgroup P of G.
Cyclic and alternating simple families
The elementary finite-simple entries are cyclic groups of prime order and A_n for n≥5.
Finite simple groups of Lie type as named families
Use the source table’s classical, exceptional, twisted, and Suzuki–Ree names without developing Lie algebras.
The twenty-six sporadic simple groups
The 26 sporadics are named exactly by the source table, with no construction or asserted pattern.
Classification of finite simple groups
Every finite simple group is cyclic of prime order, alternating of degree at least five, of Lie type, or one of 26 sporadics, with standard low-rank identifications.
Low-rank coincidences and duplicate names
Low-rank isomorphisms and exceptional parameter values are governed by the source table.
History of the first-generation classification
The first-generation classification was a multi-decade programme distributed across the literature.
The quasithin gap and its repair
The original programme required the Aschbacher–Smith quasithin classification to close a documented gap.
Status of the second-generation proof
At the task's 2026-08-14 design check, the GLS revision remained ongoing. The 2025 Oberwolfach report, organized in part by GLS collaborator Inna Capdeboscq, describes the GLS project as ongoing and nearing completion. The current AMS catalog meanwhile lists Number 10 as the tenth volume in a series whose aim is to provide a complete proof, and says that this volume completes only the bicharacteristic-type identification begun in Number 9.
Feit–Thompson odd-order theorem
Every nontrivial finite group of odd order is solvable.
Schreier’s conjecture as a CFSG consequence
Outer automorphism groups of finite simple groups are solvable.
Two-generation of finite simple groups
Every finite simple group is generated by two elements, as a CFSG-dependent result.
What the library proves and does not prove about CFSG
The library proves elementary family results and gives a source-backed proof of the local generalized-Fitting theorem, but it does not prove classification, recognition, order formulae, character tables, or sporadic constructions.
CFSG says every finite group is simple
Statement
The classification of finite simple groups says that every finite group is simple.
Facts & Assumptions
Given: Take the cyclic group .
Refutation
Its subgroup of order two is nontrivial and proper, so is not simple.
Thus a finite group need not be simple; CFSG classifies the finite groups that are simple and does not assert otherwise.
Composition factors determine the finite group
Statement
Two finite groups with the same multiset of composition factors are isomorphic.
Facts & Assumptions
Given: Compare and .
Refutation
Each has a composition series with two factors isomorphic to . However, contains an element of order four and does not.
The groups are therefore nonisomorphic despite having the same multiset of composition factors.
All finite simple groups are alternating or cyclic
Statement
Every finite simple group is cyclic or alternating.
Facts & Assumptions
Given: Use the simple Lie-type group from the cited CFSG family table.
Smith's CFSG family table records as a finite simple group of Lie type.
Refutation
This group has order . It is nonabelian, so it is not cyclic. It is not alternating: , , and for .
Hence a finite simple group can be neither cyclic nor alternating.
The library proves CFSG
Statement
This library proves the classification of finite simple groups.
Facts & Assumptions
Given: Read Classification of finite simple groups ‡ with this page's declared scope.
Refutation
That carrier records CFSG as an external landmark; it supplies no local classification proof. The page proves only its elementary component and generalized-Fitting results.
Consequently the library records the classification statement but does not prove it.
The second-generation CFSG proof is complete as of 2026
Statement
The second-generation proof of the classification of finite simple groups is complete as of 2026.
Facts & Assumptions
Given: Use the official AMS Number 10 record cited above, as checked on 2026-08-14.
The 2025 Oberwolfach report, organized in part by GLS collaborator Inna Capdeboscq, describes the GLS project as ongoing and nearing completion.
The current AMS catalog describes Number 10 as the tenth volume in a series whose aim is to provide a complete proof and says that Number 10 completes only the bicharacteristic-type identification begun in Number 9.
Refutation
The Oberwolfach report explicitly records an ongoing project, and the current AMS catalog records only the more limited completion accomplished by Number 10.
Thus the cited status evidence supports an ongoing programme, contradicting the claimed completion as of the design check.
Lie type is developed here through Lie algebras
Statement
This page develops the finite simple groups of Lie type through their Lie-algebra structure.
Facts & Assumptions
Given: Inspect the named-family carrier Finite simple groups of Lie type as named families.
Refutation
It records only the source table's family names and conventions. It does not define root data, Chevalley groups, or the Lie-algebra constructions from which the families arise.
The claim that this page develops the groups through Lie-algebra structure is therefore false.
5 · Examples, counterexamples and false statements
None yet.
Sources
- Stephen D. Smith, CFSG—A User’s Manual
- Michael Aschbacher, The Status of the Classification of the Finite Simple Groups
- American Mathematical Society, The Classification of the Finite Simple Groups, Number 10
- Capdeboscq, Henke, and Liebeck, Finite Groups, Fusion Systems and Applications, Oberwolfach Report 16/2025