Finite simple groups are generated by two elements

This repository contains a Lean 4 proof that every finite simple group is generated by two elements, using AxiomMath/CFSG's proof of the classification of finite simple groups.

Comparator/Solution.lean proves two theorems, one conditional and one unconditional.

The conditional theorem assumes the classification, stated as TauCeti's ClassificationStatement (every finite simple group is isomorphic to one on TauCeti's list).

theorem CFSGCorollary.exists_closure_pair_eq_top_of_classification
    (hCFSG : TauCeti.ClassificationStatement.{0}) (G : Type u) [Group G] [Finite G]
    [IsSimpleGroup G] : ∃ a b : G, Subgroup.closure {a, b} = ⊤

The unconditional theorem applies the conditional theorem to CFSG's proof of the classification, CFSG.Certified.classification_finite_simple_groups.

theorem CFSGCorollary.exists_closure_pair_eq_top (G : Type u) [Group G] [Finite G]
    [IsSimpleGroup G] : ∃ a b : G, Subgroup.closure {a, b} = ⊤

• Most of the work is in the CFSGCorollary library, which proves that every group on TauCeti's list (cyclic of prime order, alternating, of Lie type, or one of the 26 sporadic groups) is generated by two elements.
• Both theorems depend only on propext, Classical.choice and Quot.sound.
• The development consists of ~18,600 lines of Lean, excluding dependencies.

Built on

• R. Steinberg, Generators for simple groups, Canad. J. Math. 14 (1962) 277–283: the groups of Lie type
• AxiomMath/CFSG: the classification, and models of the groups on the list, identified with TauCeti's carriers
• TauCeti: the classification statement and the list
• Mathlib

The proof

The classification gives G ≃* i.Group for an index i on TauCeti's list, and two-generation transfers along isomorphisms, so it suffices to treat each family.

• Cyclic: generated by one element.
• Alternating: a 3-cycle and an n- or (n - 1)-cycle generate a primitive group containing a 3-cycle, hence the alternating group by Jordan's theorem (Mathlib).
• Sporadic: CFSG gives each as the closure of two permutations or the units of a monoid generated by two matrices; for the Monster, two explicit products of the generators of TauCeti's Coxeter-type presentation suffice.
• Lie type: Steinberg's Lemmas 3.9, 3.10 and 3.12, proved once for abstract root group systems and instantiated on CFSG's models: SL, Sp, Spin and the adjoint exceptional groups (untwisted); SU, minus-type Spin, ³D₄, ²E₆, Suzuki, and small and large Ree groups (twisted). The Tits group is the closure of two permutations.

Directory	Contents
CFSGCorollary/TwoGenerated	two-generation and its transfer along isomorphisms and surjections
CFSGCorollary/Cyclic.lean, Alternating, Sporadic	cyclic, alternating and sporadic groups
CFSGCorollary/LieType/Steinberg	Steinberg's Lemmas 3.9–3.12 for root group systems
CFSGCorollary/LieType/LambdaRootGroup	the same, for root groups coordinatized over a finite field (twisted groups)
CFSGCorollary/LieType/Chevalley	untwisted groups on CFSG's models: root computations (Roots) and generation (Generation) per Cartan type
CFSGCorollary/LieType/Twisted	²A, ²D, ³D₄, ²E₆, Suzuki, small and large Ree groups
CFSGCorollary/CFSGIndex.lean	every group on TauCeti's list is two-generated
Checks	checks that the conditional theorem avoids the classification proof
Comparator/Solution.lean	both theorems
Comparator/Challenge.lean	the statements, for comparator

Build

The build uses Lean v4.35.0-rc3. Mathlib and TauCeti are pinned to the revisions CFSG uses.

CFSG publishes prebuilt files for Linux x86_64 only, and they take about 230 GB of disk. To download them, along with Mathlib's and TauCeti's, and build:

ulimit -s 1048576
export RUST_MIN_STACK=1073741824 LAKE_ARTIFACT_CACHE=true
curl -fsSLO https://cfsg-downloads.axiommath.workers.dev/lake/lake-cache-get-fast.sh
bash lake-cache-get-fast.sh .
lake build

On other platforms, Lake compiles the parts of CFSG it needs from source.

If you have built any Mathlib module yourself with this toolchain, the downloaded files won't match and Lake will rebuild CFSG from source. To avoid this, start with an empty Lake cache (~/.elan/toolchains/<toolchain>/lake/cache) and .lake directory.

The build prints the axioms each theorem depends on, and two expected sorry warnings from Comparator/Challenge.lean. To build only the library, run lake build CFSGCorollary. It doesn't import CFSG's proof of the classification.

comparator.json lists both theorems, but neither has been checked with comparator (due to time constraints).

Licensed under Apache-2.0.