Classification of Finite Simple Groups in Lean

• Website

A sorry-free Lean4 (v4.35.0-rc3) proof of the Classification of Finite Simple Groups (CFSG), built on Mathlib and TauCeti, using the standard axioms Classical.choice, propext, and Quot.sound (no native_decide). We primarily follow the first generation proof of CFSG.

We use the statement of CFSG from the TauCeti project

/-- **Classification of finite simple groups, statement only.** Every finite simple group is
isomorphic to one of the explicitly constructed groups on the classification list. -/
def ClassificationStatement : Prop :=
  ∀ (G : Type u) [Group G] [Finite G] [IsSimpleGroup G],
    ∃ i : CFSGIndex, Nonempty (G ≃* i.Group)

Checking the proof

lake build builds the entire project. We used a few open changes to Lake and some optimizations we plan to upstream soon to get this project's build time under 24 hours.

License

APACHE-2.0