feat: add six finite-group-theory benchmark problems

LeanEval/GroupTheory/Frobenius.lean

@@ -0,0 +1,35 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace GroupTheory
+
+/-!
+Frobenius's theorem on Frobenius groups.
+
+A *Frobenius group* is a finite group `G` acting transitively and faithfully on
+a set `X` (with `|X| ≥ 2`) such that:
+* point stabilisers are non-trivial, and
+* no non-identity element of `G` fixes more than one point of `X`.
+
+Frobenius's theorem (1901) states that the *Frobenius kernel*
+  `K = {1} ∪ {g ∈ G | g fixes no point of X}`
+is a normal subgroup of `G`. The only known proof uses character theory
+(induction of characters from a point stabiliser to `G`); no purely
+group-theoretic proof has been found in over a century.
+-/
+
+@[eval_problem]
+theorem frobenius_kernel_isNormal
+    (G X : Type) [Group G] [Fintype G] [Fintype X]
+    [MulAction G X] [FaithfulSMul G X]
+    (hcard : 2 ≤ Fintype.card X)
+    (htrans : ∀ x y : X, ∃ g : G, g • x = y)
+    (hstab : ∀ x : X, MulAction.stabilizer G x ≠ ⊥)
+    (hfrob : ∀ g : G, g ≠ 1 → ∀ x y : X, g • x = x → g • y = y → x = y) :
+    ∃ N : Subgroup G, N.Normal ∧
+      (N : Set G) = {1} ∪ {g : G | ∀ x : X, g • x ≠ x} := by
+  sorry
+
+end GroupTheory
+end LeanEval

LeanEval/GroupTheory/GlaubermanZStar.lean

@@ -0,0 +1,39 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace GroupTheory
+
+/-!
+Glauberman's `Z*`-theorem (1966).
+
+Let `G` be a finite group and let `t ∈ G` be an *isolated involution*: an
+element of order 2 such that no conjugate of `t` (other than `t` itself)
+commutes with `t`. Then `t` is central in `G / O(G)`, where `O(G)` is the
+largest normal subgroup of `G` of odd order.
+
+Equivalently: there exists a normal subgroup `N ⊴ G` of odd order such that
+every multiplicative commutator `g * t * g⁻¹ * t⁻¹` lies in `N`.
+
+The hypothesis below is the *global* form of isolation ("no distinct conjugate
+of `t` commutes with `t`"). This is equivalent to the more familiar local form
+("`t` is the unique involution of a Sylow 2-subgroup of `C_G(t)`"), but is
+self-contained and avoids reference to Sylow theory in the statement.
+
+The proof is a deep application of modular (Brauer) representation theory and
+is a cornerstone of the classification of finite simple groups: it is what
+allows the local analysis to "fuse" 2-elements via odd-order normal subgroups.
+-/
+
+@[eval_problem]
+theorem glauberman_zStar
+    (G : Type) [Group G] [Fintype G]
+    (t : G) (ht1 : t ≠ 1) (ht2 : t * t = 1)
+    (hisolated : ∀ g : G, (g * t * g⁻¹) * t = t * (g * t * g⁻¹) →
+      g * t * g⁻¹ = t) :
+    ∃ N : Subgroup G, N.Normal ∧ Odd (Nat.card N) ∧
+      ∀ g : G, g * t * g⁻¹ * t⁻¹ ∈ N := by
+  sorry
+
+end GroupTheory
+end LeanEval

LeanEval/GroupTheory/MultiplyTransitive.lean

@@ -0,0 +1,45 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace GroupTheory
+
+/-!
+Classification of `5`-transitive finite permutation groups (uses CFSG).
+
+If a finite group `G` acts faithfully and `5`-transitively on a set `X` of
+cardinality `n ≥ 5`, then `|G|` is one of:
+
+* `n!`             (`G ≅ Sₙ`,    any `n ≥ 5`)
+* `n! / 2`         (`G ≅ Aₙ`,    any `n ≥ 7`)
+* `95 040`         (`G ≅ M₁₂`,    `n = 12`)
+* `244 823 040`    (`G ≅ M₂₄`,    `n = 24`)
+
+These are the only `5`-transitive finite groups. The result is folklore via
+the classification of finite simple groups: it follows from CFSG together with
+classical work of Mathieu, Jordan, and others. No CFSG-free proof is known.
+
+The `5 ≤ Fintype.card X` hypothesis prevents the `5`-transitivity condition
+from being vacuously satisfied (otherwise any small action — e.g. `C₃` on
+`Fin 3` — would qualify, since there are no injective maps `Fin 5 → X`).
+
+The companion `4`-transitive classification additionally allows
+`M₁₁` (`n = 11`, `|G| = 7920`) and `M₂₃` (`n = 23`, `|G| = 10 200 960`).
+-/
+
+@[eval_problem]
+theorem 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) := by
+  sorry
+
+end GroupTheory
+end LeanEval

LeanEval/GroupTheory/SchreierConjecture.lean

@@ -0,0 +1,41 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace GroupTheory
+
+/-!
+Schreier's conjecture (theorem, modulo CFSG).
+
+For every finite non-abelian simple group `S`, the outer automorphism group
+`Out(S) := Aut(S) / Inn(S)` is solvable.
+
+This was conjectured by Schreier in the 1920s. It is verified case-by-case
+through the classification of finite simple groups: for each family
+(alternating, classical, exceptional Lie type, sporadic) one inspects `Out(S)`
+and observes solvability. No CFSG-free proof is known.
+
+`MulAut.conj : S →* MulAut S` sends `s ↦ (conjugation by s)`; its range is
+`Inn(S)`. The instance below records that `Inn(S)` is normal in `Aut(S)`,
+which is needed to form the quotient.
+-/
+
+/-- `Inn(S)` is a normal subgroup of `Aut(S)`: the conjugate of `conj s` by an
+automorphism `α` is `conj (α s)`. -/
+instance innNormal (S : Type*) [Group S] :
+    ((MulAut.conj : S →* MulAut S).range).Normal where
+  conj_mem := by
+    rintro _ ⟨s, rfl⟩ α
+    refine ⟨α s, ?_⟩
+    ext x
+    simp [MulAut.conj_apply, map_mul, map_inv, MulEquiv.apply_symm_apply]
+
+@[eval_problem]
+theorem schreier_conjecture
+    (S : Type) [Group S] [Fintype S] [IsSimpleGroup S]
+    (hS : ∃ a b : S, ¬ Commute a b) :
+    IsSolvable (MulAut S ⧸ (MulAut.conj : S →* MulAut S).range) := by
+  sorry
+
+end GroupTheory
+end LeanEval

LeanEval/RepresentationTheory/BrauerSplittingField.lean

@@ -0,0 +1,39 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace RepresentationTheory
+
+/-!
+Brauer's theorem on character values.
+
+For a finite group `G` of exponent `n`, every value of every complex
+character of `G` lies in (the image of) the cyclotomic field `ℚ(ζₙ)`.
+Concretely: there is a ring embedding `φ : ℚ(ζₙ) →+* ℂ` whose range
+contains `tr ρ(g)` for every finite-dimensional complex representation
+`ρ` of `G` and every `g ∈ G`.
+
+This is a consequence of Brauer's induction theorem (every character is a
+ℤ-combination of characters induced from elementary subgroups, whose values
+are visibly cyclotomic).
+
+The full Brauer "splitting field" theorem says more — that `ℚ(ζₙ)` is in fact
+a *splitting field* for the group algebra, i.e. every irreducible complex
+representation admits a `ℚ(ζₙ)`-form. The character-value statement below
+is implied by the splitting-field statement and is the part most cleanly
+expressible in Mathlib's current API; the full splitting-field statement
+would additionally require scalar-extension scaffolding around
+`CyclotomicField n ℚ → ℂ`.
+-/
+
+@[eval_problem]
+theorem brauer_character_in_cyclotomic
+    (G : Type) [Group G] [Fintype G] :
+    ∃ φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ,
+      ∀ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V)
+        (ρ : Representation ℂ G V) (g : G),
+        LinearMap.trace ℂ V (ρ g) ∈ φ.range := by
+  sorry
+
+end RepresentationTheory
+end LeanEval

LeanEval/RepresentationTheory/M23TensorSquare.lean

@@ -0,0 +1,63 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace RepresentationTheory
+
+open scoped TensorProduct
+
+/-!
+Existential tensor-square problem for the Mathieu group `M₂₃`.
+
+We assert the existence of a finite group `G` of order `|M₂₃| = 10 200 960`,
+together with a `22`-dimensional irreducible complex representation `V`,
+such that the tensor square `V ⊗ V` (with the diagonal `G`-action) decomposes
+into exactly `4` isotypic components.
+
+Mathematical witness. Take `G = M₂₃` acting on the deleted permutation
+representation of its 4-transitive action on 23 points. Let `V` be the
+corresponding 22-dimensional irreducible. Then
+* `Sym² V` is the permutation representation on the `(23 choose 2) = 253`
+  unordered pairs, decomposing as `1 ⊕ V ⊕ W` where `W` is a 230-dimensional
+  irreducible.
+* `Λ² V` is irreducible of dimension `231` (one of the three 231-dim irreps).
+
+So `V ⊗ V = 1 ⊕ V ⊕ W ⊕ Λ²V` has exactly four pairwise non-isomorphic
+irreducible summands.
+
+Mathlib does not yet construct `M₂₃` directly, so any solution must build the
+group from scratch (e.g. as a subgroup of `S₂₃` via generators of the Steiner
+system `S(4,7,23)`, or from the automorphism group of an extended ternary Golay
+code, etc.). The statement does not pin down `M₂₃` uniquely (other groups of
+the same order with a 22-dim irrep of the right tensor-square structure would
+also satisfy the existential), but while this does not technically require
+constructing `M₂₃` and studying its representation theory, we suspect that in
+practice it does.
+
+The `MonoidAlgebra ℂ G`-module structures on `V` and `V ⊗[ℂ] V` are bound
+explicitly. The `IsScalarTower` constraints anchor them to the underlying
+ℂ-module structures, and the explicit diagonal-action equation pins the
+`V ⊗ V` action to be `g • (v ⊗ w) = (g • v) ⊗ (g • w)` (extended ℂ-linearly
+to the whole group algebra by ℂ-bilinearity of the tensor).
+-/
+
+@[eval_problem]
+theorem m23_irrep_tensor_square_decomp :
+    ∃ (G : Type) (_ : Group G) (_ : Fintype G),
+      Fintype.card G = 10200960 ∧
+      ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V)
+        (_ : Module (MonoidAlgebra ℂ G) V)
+        (_ : IsScalarTower ℂ (MonoidAlgebra ℂ G) V)
+        (_ : Module (MonoidAlgebra ℂ G) (V ⊗[ℂ] V))
+        (_ : IsScalarTower ℂ (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)),
+        Module.finrank ℂ V = 22 ∧
+        IsSimpleModule (MonoidAlgebra ℂ G) V ∧
+        (∀ (g : G) (v w : V),
+          (MonoidAlgebra.of ℂ G g : MonoidAlgebra ℂ G) • (v ⊗ₜ[ℂ] w) =
+            ((MonoidAlgebra.of ℂ G g : MonoidAlgebra ℂ G) • v) ⊗ₜ[ℂ]
+              ((MonoidAlgebra.of ℂ G g : MonoidAlgebra ℂ G) • w)) ∧
+        (isotypicComponents (MonoidAlgebra ℂ G) (V ⊗[ℂ] V)).ncard = 4 := by
+  sorry
+
+end RepresentationTheory
+end LeanEval

manifests/problems.toml

@@ -413,3 +413,69 @@ holes = ["WidgetCarrier", "instInhabitedWidget"]
 submitter = "Kim Morrison"
 notes = "Minimal example exercising instance + theorem holes; instances must be named so the comparator can address them."
 
+
+[[problem]]
+id = "brauer_character_in_cyclotomic"
+title = "Character values of finite groups lie in cyclotomic fields"
+test = false
+module = "LeanEval.RepresentationTheory.BrauerSplittingField"
+holes = ["brauer_character_in_cyclotomic"]
+submitter = "Kim Morrison"
+notes = "For a finite group G of exponent n, every value of every complex character of G lies in (the image of) the cyclotomic field ℚ(ζₙ). Stated uniformly for the fixed group G: there is a ring embedding φ : CyclotomicField (Monoid.exponent G) ℚ →+* ℂ whose range contains tr(ρ(g)) for every finite-dimensional complex representation ρ of G and every g. This is a corollary of Brauer's induction theorem; the full splitting-field statement (every irreducible representation has a ℚ(ζₙ)-form) is strictly stronger and requires more scalar-extension scaffolding than mathlib currently exposes cleanly."
+source = "R. Brauer, On the representation of a group of order g in the field of g-th roots of unity, Amer. J. Math. 67 (1945)."
+informal_solution = "Choose an embedding φ : ℚ(ζₙ) ↪ ℂ once and for all for the fixed group G. Then apply Brauer's induction theorem uniformly: every complex character of G is a ℤ-combination of characters induced from elementary subgroups, and those induced character values lie in φ(ℚ(ζₙ)). Hence for every finite-dimensional complex representation ρ of G and every g ∈ G, tr(ρ(g)) lies in φ.range."
+
+[[problem]]
+id = "m23_irrep_tensor_square_decomp"
+title = "Existence of an order-10200960 group with a 22-dim irrep whose tensor square has 4 isotypic components"
+test = false
+module = "LeanEval.RepresentationTheory.M23TensorSquare"
+holes = ["m23_irrep_tensor_square_decomp"]
+submitter = "Kim Morrison"
+notes = "Existential: a finite group G of order 10200960 (= |M₂₃|) with a 22-dimensional irreducible complex representation V whose tensor square (with the diagonal G-action) has exactly 4 isotypic components. Both the MonoidAlgebra ℂ G action on V and on V ⊗[ℂ] V are bound explicitly, with IsScalarTower and an explicit diagonal-action equation g•(v⊗w) = (g•v)⊗(g•w) pinning the V⊗V action. The intended witness is M₂₃ acting on its 22-dim irreducible: V ⊗ V = 1 ⊕ V ⊕ W₂₃₀ ⊕ Λ²V. While the formal statement does not technically require constructing M₂₃ and studying its representation theory, we suspect that in practice it does."
+source = "É. Mathieu, Sur les fonctions cinq fois transitives de 24 quantités, J. Math. Pures Appl. (1873); ATLAS of Finite Groups, M₂₃ character table."
+informal_solution = "Realise M₂₃ as a subgroup of S₂₃ (e.g. via the Steiner system S(4,7,23) or as the automorphism group of a ternary Golay code construction). Take V to be the 22-dimensional deleted permutation representation. By 4-transitivity Sym²V is the permutation representation on the 23 choose 2 = 253 unordered pairs, decomposing as 1 + V + W₂₃₀ where W is the unique 230-dimensional irrep; Λ²V is irreducible of dimension 231, giving four pairwise non-isomorphic isotypic components in V⊗V."
+
+[[problem]]
+id = "frobenius_kernel_isNormal"
+title = "Frobenius's theorem: the Frobenius kernel is normal"
+test = false
+module = "LeanEval.GroupTheory.Frobenius"
+holes = ["frobenius_kernel_isNormal"]
+submitter = "Kim Morrison"
+notes = "For a Frobenius group G acting transitively and faithfully on X with |X| ≥ 2, non-trivial point stabilisers, and the Frobenius condition (no non-identity element fixes more than one point), the set {1} ∪ {g | g fixes no point} is a normal subgroup. The only known proof uses Frobenius's induction-of-characters argument; no purely group-theoretic proof has been found in over a century."
+source = "G. Frobenius, Über auflösbare Gruppen IV, Sitzungsber. Akad. Wiss. Berlin (1901)."
+informal_solution = "Let H = stabilizer(x₀). Construct a class function θ on H of the form (1_H minus restriction of certain induced characters), and apply Frobenius reciprocity to lift θ to a generalised character of G whose kernel is exactly the Frobenius kernel K. The fact that the lift remains a virtual character (i.e. integer-valued combination of irreducibles) is exactly the content; that K is then a subgroup follows from K being a kernel."
+
+[[problem]]
+id = "glauberman_zStar"
+title = "Glauberman's Z* theorem for isolated involutions"
+test = false
+module = "LeanEval.GroupTheory.GlaubermanZStar"
+holes = ["glauberman_zStar"]
+submitter = "Kim Morrison"
+notes = "For a finite group G with an isolated involution t (no distinct conjugate of t commutes with t), there is a normal subgroup N ⊴ G of odd order such that every commutator g·t·g⁻¹·t⁻¹ lies in N — i.e., t is central in G/N. The hypothesis is the global form of isolation, equivalent to (but more self-contained than) the standard Sylow-local form. Proof uses modular Brauer character theory."
+source = "G. Glauberman, Central elements in core-free groups, J. Algebra 4 (1966)."
+informal_solution = "Take N = O(G), the largest normal subgroup of odd order. By Glauberman's modular character argument, isolation of t in C_G(t) implies t commutes with every element of G modulo O(G). The core of the proof is the analysis of the principal 2-block of G via Brauer characters and the Z*-style fusion theorem."
+
+[[problem]]
+id = "schreier_conjecture"
+title = "Schreier's conjecture: outer automorphism group of a finite simple group is solvable"
+test = false
+module = "LeanEval.GroupTheory.SchreierConjecture"
+holes = ["schreier_conjecture"]
+submitter = "Kim Morrison"
+notes = "For every finite non-abelian simple group S, Out(S) := Aut(S)/Inn(S) is solvable. The statement requires the normality of Inn(S) ⊴ Aut(S), which is supplied by a local instance with a one-line proof (the conjugate of conj(s) by α equals conj(α(s))). Verified case-by-case via CFSG; no CFSG-free proof is known."
+source = "O. Schreier, Über die Erweiterung von Gruppen II, Abh. Math. Sem. Univ. Hamburg 4 (1926); CFSG, completed c. 2004."
+informal_solution = "Use the classification of finite simple groups. For each family — alternating Aₙ, classical Lie type, exceptional Lie type, sporadic — inspect the known Out(S) and verify it is solvable. For Aₙ (n ≥ 5, n ≠ 6), Out = ℤ/2; for A₆, Out = (ℤ/2)²; for groups of Lie type, Out is built from diagonal, field, and graph automorphisms (each step solvable); for sporadics, Out is trivial or ℤ/2."
+
+[[problem]]
+id = "five_transitive_card_classification"
+title = "Possible orders of 5-transitive finite permutation groups"
+test = false
+module = "LeanEval.GroupTheory.MultiplyTransitive"
+holes = ["five_transitive_card_classification"]
+submitter = "Kim Morrison"
+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."