The classification of finite simple groups | Lean AI formalization leaderboard

Problem statement

Notes: Every finite simple group is isomorphic to a cyclic group of prime order, an alternating group Aₙ with n ≥ 5, a group of Lie type, or one of the twenty-six sporadic groups. The list is the Tau Ceti project's TauCeti.CFSGIndex, and the statement is TauCeti.ClassificationStatement spelled out. The Lie-type groups are explicit constructions (the derived subgroup of the fixed points of a Steinberg endomorphism, modulo its centre), and the sporadic groups are given by explicit finite presentations; the problem inherits the correctness of those definitions from Tau Ceti. Only the direction 'every finite simple group is on the list' is required: finiteness, simplicity and irredundancy of the listed groups are not part of the statement.

Source: D. Gorenstein, R. Lyons and R. Solomon, The Classification of the Finite Simple Groups (AMS Mathematical Surveys and Monographs 40, 1994–); M. Aschbacher, R. Lyons, S. D. Smith and R. Solomon, The Classification of Finite Simple Groups: Groups of Characteristic 2 Type (AMS, 2011). Statement: https://github.com/TauCetiProject/TauCeti/blob/main/TauCeti/GroupTheory/SpecificGroups/CFSG/Classification.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`classification_finite_simple_groups (G : Type) [Group G] [Finite G] [IsSimpleGroup G] :
    ∃ i : TauCeti.CFSGIndex, Nonempty (G ≃* i.Group) := byG:Typeinst✝²:Group Ginst✝¹:Finite Ginst✝:IsSimpleGroup G⊢ ∃ i, Nonempty (G ≃* i.Group)
  sorryAll goals completed! 🐙