From c35e52d4ab0ccfccfceedc0cb3d9cc18da7fbbf2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 24 May 2026 07:01:16 +0000
Subject: [PATCH] feat: add Brauer-Fowler theorem eval problem
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds the Brauer-Fowler theorem (1955): the order of a finite
nonabelian simple group is bounded by a function of the order of any
involution centralizer. A foundational organising principle of the
CFSG programme, reducing the classification (in principle) to the
analysis of involution centralizers.

Statement uses only Mathlib — no new definitions.

🤖 Prepared with Claude Code
---
 LeanEval/GroupTheory/BrauerFowler.lean | 44 ++++++++++++++++++++++++++
 manifests/problems.toml                | 12 +++++++
 2 files changed, 56 insertions(+)
 create mode 100644 LeanEval/GroupTheory/BrauerFowler.lean

diff --git a/LeanEval/GroupTheory/BrauerFowler.lean b/LeanEval/GroupTheory/BrauerFowler.lean
new file mode 100644
index 0000000..1d1f9b4
--- /dev/null
+++ b/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
diff --git a/manifests/problems.toml b/manifests/problems.toml
index 87a63eb..e6e1ca5 100644
--- a/manifests/problems.toml
+++ b/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."
+