Possible orders of 5-transitive finite permutation groups

Problem statement

Notes: If a finite group acts faithfully and 5-transitively on a set X with |X| ≥ 5, then |G| is one of n!, n!/2 (only when n ≥ 7), 95040 (= |M₁₂|), or 244823040 (= |M₂₄|). The 5 ≤ |X| hypothesis prevents the 5-transitivity condition from being vacuously satisfied (otherwise small groups like C₃ on Fin 3 would qualify). Classification is folklore via CFSG; no CFSG-free proof is known.

Source: Folklore via CFSG; classical work of Mathieu, Jordan; modern accounts in P. Cameron, Permutation Groups (1999).

Informal solution: By CFSG, the only finite 2-transitive groups are explicitly classified. Restricting to 5-transitive: the symmetric group Sₙ is k-transitive for all k ≤ n; the alternating group Aₙ is k-transitive for k ≤ n − 2 (so 5-transitive for n ≥ 7); among the Mathieu groups, M₁₂ is sharply 5-transitive on 12 points and M₂₄ is 5-transitive on 24 points. M₁₁ and M₂₃ are only 4-transitive and so do not appear. No other finite simple group has a 5-transitive permutation representation.

theorem declaration uses `sorry`five_transitive_card_classification (G X : Type) [Group G] [Fintype G] [Fintype X]
    [MulAction G X] [FaithfulSMul G X]
    (hcard : 5 ≤ Fintype.card X)
    (h5 : ∀ a b : Fin 5 → X, Function.Injective a → Function.Injective b →
      ∃ g : G, ∀ i, g • a i = b i) :
    let n := Fintype.card X
    Fintype.card G = n.factorial ∨
    (7 ≤ n ∧ Fintype.card G = n.factorial / 2) ∨
    (n = 12 ∧ Fintype.card G = 95040) ∨
    (n = 24 ∧ Fintype.card G = 244823040) := byG:TypeX:Typeinst✝⁴:Group Ginst✝³:Fintype Ginst✝²:Fintype Xinst✝¹:MulAction G Xinst✝:FaithfulSMul G Xhcard:5 ≤ Fintype.card Xh5:∀ (a b : Fin 5 → X), Function.Injective a → Function.Injective b → ∃ g, ∀ (i : Fin 5), g • a i = b i⊢ let n := Fintype.card X;
Fintype.card G = n.factorial ∨
  7 ≤ n ∧ Fintype.card G = n.factorial / 2 ∨ n = 12 ∧ Fintype.card G = 95040 ∨ n = 24 ∧ Fintype.card G = 244823040
  sorryAll goals completed! 🐙