feat: add Brauer-Fowler theorem eval problem

LeanEval/GroupTheory/BrauerFowler.lean

@@ -0,0 +1,44 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace GroupTheory
+
+/-!
+# Brauer–Fowler theorem
+
+Let `G` be a finite simple group with an involution `t`. Then `|G|` is
+bounded by a function of `|C_G(t)|` alone. Equivalently: for each `n`,
+only finitely many finite nonabelian simple groups have an involution
+whose centralizer has order `n`.
+
+Stated by Richard Brauer in 1954 (with Fowler) as a key motivation for
+the project of classifying finite simple groups: it reduces the
+classification (in principle) to studying involution centralizers, a
+much smaller class of groups. The first general involution-centralizer
+analyses (Brauer–Suzuki, Brauer–Suzuki–Wall, Janko) used this principle
+to discover several sporadic simple groups, and it remained one of the
+central organising ideas of the CFSG programme.
+
+The bound `f` is not specified — any concrete bound suffices, the
+classical Brauer–Fowler bound being roughly `(n^2)!`. The statement
+quantifies over all finite simple groups `G` in a fixed universe.
+
+The proof is short and uses only counting / orbit-counting arguments
+together with the observation that any two involutions generate a
+dihedral subgroup; no deep machinery is required.
+-/
+
+/-- **Brauer–Fowler theorem.** There is a function bounding the order
+of a finite nonabelian simple group by the order of any involution
+centralizer. -/
+@[eval_problem]
+theorem 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
+  sorry
+
+end GroupTheory
+end LeanEval

manifests/problems.toml

@@ -682,3 +682,15 @@ module = "LeanEval.Geometry.Uniformization"
 holes = ["uniformization"]
 submitter = "Junyan Xu"
 source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1."
+
+[[problem]]
+id = "brauer_fowler"
+title = "Brauer–Fowler theorem"
+test = false
+module = "LeanEval.GroupTheory.BrauerFowler"
+holes = ["brauer_fowler"]
+submitter = "Kim Morrison"
+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."
+