Brauer–Fowler theorem | Lean AI formalization leaderboard

Problem statement

Notes: The order of a finite nonabelian simple group is bounded by a function of the order of any involution centralizer. R. Brauer and K. A. Fowler, 'On groups of even order', Ann. of Math. 62 (1955), 565-583. A foundational result of the CFSG programme: it reduced (in principle) the classification of finite simple groups to the analysis of involution centralizers — the strategy used by Brauer–Suzuki, Brauer–Suzuki–Wall, Janko, and many others to identify sporadic simple groups. Statement uses only Mathlib (IsSimpleGroup, Nat.card, Subgroup.centralizer, orderOf), no new definitions.

Source: R. Brauer and K. A. Fowler, On groups of even order, Ann. of Math. (2) 62 (1955), 565-583. https://doi.org/10.2307/1970080

Informal solution: Counting argument. For an involution t in a finite simple group G with C := |C_G(t)|, every pair of involutions a, b generates a dihedral subgroup ⟨a,b⟩ of order 2k for some k ≥ 1; the product ab has order k. Use the class equation and orbit-counting on conjugates of t to show that |G| divides (2C^2)! or a similar explicit factorial of a polynomial in C — any such bound furnishes the required f.

theorem declaration uses `sorry`brauer_fowler :
    ∃ f : ℕ → ℕ, ∀ (G : Type) [Group G] [Finite G],
      IsSimpleGroup G → (∃ a b : G, a * b ≠ b * a) →
      ∀ t : G, orderOf t = 2 →
        Nat.card G ≤ f (Nat.card (Subgroup.centralizer ({t} : Set G))) := by⊢ ∃ f,
  ∀ (G : Type) [inst : Group G] [Finite G],
    IsSimpleGroup G →
      (∃ a b, a * b ≠ b * a) → ∀ (t : G), orderOf t = 2 → Nat.card G ≤ f (Nat.card ↥(Subgroup.centralizer {t}))
  sorryAll goals completed! 🐙