From 69a34f1b9905d7c5a44a1d440d6173fdb6be7cc6 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 2 Jun 2026 05:40:36 +0000 Subject: [PATCH 1/2] feat: add Higman infinite finitely-presented simple group eval problem Co-Authored-By: Claude Opus 4.7 --- .../GroupTheory/HigmanInfiniteSimple.lean | 35 +++++++++++++++++++ .../problems/higman_infinite_simple.toml | 9 +++++ 2 files changed, 44 insertions(+) create mode 100644 LeanEval/GroupTheory/HigmanInfiniteSimple.lean create mode 100644 manifests/problems/higman_infinite_simple.toml diff --git a/LeanEval/GroupTheory/HigmanInfiniteSimple.lean b/LeanEval/GroupTheory/HigmanInfiniteSimple.lean new file mode 100644 index 0000000..a9eb7ba --- /dev/null +++ b/LeanEval/GroupTheory/HigmanInfiniteSimple.lean @@ -0,0 +1,35 @@ +import Mathlib +import EvalTools.Markers + +namespace LeanEval +namespace GroupTheory +namespace HigmanInfiniteSimpleProblem + +/-! +# Higman's infinite finitely-presented simple group + +There exists an infinite, finitely presented, simple group. Graham +Higman gave the first example in 1951; a much shorter construction +appears in Higman's 1974 monograph *Finitely Presented Infinite Simple +Groups*. §122 in Knill's *Some Fundamental Theorems in Mathematics*. + +Concretely: some `n` and a finite relator set +`rels ⊆ FreeGroup (Fin n)` for which `PresentedGroup rels` is both +simple and infinite. Pure existence of a pathological finite +presentation. Mathlib has `FreeGroup`, `PresentedGroup`, +`IsSimpleGroup`, and `Infinite`, but no construction of any infinite +finitely-presented simple group. +-/ + +/-- **Higman's infinite simple group** (G. Higman 1951/1974). There +exists an infinite finitely presented simple group. -/ +@[eval_problem] +theorem higman_infinite_simple : + ∃ (n : ℕ) (rels : Set (FreeGroup (Fin n))), + rels.Finite ∧ IsSimpleGroup (PresentedGroup rels) ∧ + Infinite (PresentedGroup rels) := by + sorry + +end HigmanInfiniteSimpleProblem +end GroupTheory +end LeanEval diff --git a/manifests/problems/higman_infinite_simple.toml b/manifests/problems/higman_infinite_simple.toml new file mode 100644 index 0000000..aec4888 --- /dev/null +++ b/manifests/problems/higman_infinite_simple.toml @@ -0,0 +1,9 @@ +id = "higman_infinite_simple" +title = "Higman's infinite finitely-presented simple group" +test = false +module = "LeanEval.GroupTheory.HigmanInfiniteSimple" +holes = ["higman_infinite_simple"] +submitter = "Kim Morrison" +notes = "There exists an infinite, finitely presented, simple group: some n and a finite relator set rels ⊆ FreeGroup (Fin n) for which PresentedGroup rels is both simple and infinite. Pure existence of a pathological finite presentation. Mathlib has FreeGroup, PresentedGroup, IsSimpleGroup, and Infinite, but no construction of any infinite finitely-presented simple group. §122 of Knill's *Some Fundamental Theorems in Mathematics*." +source = "G. Higman, 'A finitely generated infinite simple group', J. London Math. Soc. 26 (1951) 61–64; G. Higman, *Finitely Presented Infinite Simple Groups*, Notes on Pure Mathematics 8, Australian National University, 1974. §122 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf)." +informal_solution = "Higman's 1951 group is built from four generators `a, b, c, d` with relations expressing that conjugation cycles through them as `b · a = a²·b`, `c · b = b²·c`, `d · c = c²·d`, `a · d = d²·a` — a `chain of squarings'. Higman proves (i) this group is finitely presented by construction; (ii) it is infinite by a combinatorial argument tracking the lengths of normal forms under the cyclic conjugation; (iii) it is simple by Britton's lemma applied to the HNN-extension decomposition implicit in the relators (any normal subgroup containing a nontrivial element must contain the whole group). The 1974 monograph gives a different, shorter construction via Higman's embedding theorem applied to a Boone–Higman simulation of a Turing machine with halting set inside the simple group. Mathlib has the substrate (`FreeGroup`, `PresentedGroup`, `IsSimpleGroup`, `Infinite`, normal closures via `Subgroup.IsNormalClosureFG`) but no HNN extensions, no Britton's lemma, no Higman embedding theorem, and no construction of an infinite finitely-presented simple group." From 07864f62af34fdf9534afa3c8c6390d7c61f0464 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 3 Jun 2026 04:53:52 +0000 Subject: [PATCH 2/2] =?UTF-8?q?fix:=20correct=201951-vs-1974=20attribution?= =?UTF-8?q?=20+=20mathlib=20HNN=20claim=20on=20=C2=A7122=20Higman?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex review of PR #384 confirmed faithfulness of the formal statement (existential shape correct; IsSimpleGroup includes Nontrivial so trivial-presentation witnesses are excluded; no vacuous-truth exploit) and caught two real errors. (1) My prior text claimed Higman's 1951 group was finitely presented and simple; in fact the 1951 paper constructs a finitely *generated* infinite simple group as a simple quotient of the four-generator "chain of squarings" group with no nontrivial finite quotients — the simple quotient need not be finitely presented. The first infinite finitely-presented simple groups are the Higman–Thompson groups G_{n,r} from Higman's 1974 monograph. Rewrote docstring + manifest accordingly. (2) Same HNN/Britton fix as #383: mathlib v4.30 DOES have HNN extensions and Britton's lemma in `Mathlib/GroupTheory/HNNExtension.lean'; corrected the "mathlib lacks X" list. Co-Authored-By: Claude Opus 4.7 --- .../GroupTheory/HigmanInfiniteSimple.lean | 19 ++++++++++++------- .../problems/higman_infinite_simple.toml | 4 ++-- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/LeanEval/GroupTheory/HigmanInfiniteSimple.lean b/LeanEval/GroupTheory/HigmanInfiniteSimple.lean index a9eb7ba..75df9f2 100644 --- a/LeanEval/GroupTheory/HigmanInfiniteSimple.lean +++ b/LeanEval/GroupTheory/HigmanInfiniteSimple.lean @@ -8,17 +8,22 @@ namespace HigmanInfiniteSimpleProblem /-! # Higman's infinite finitely-presented simple group -There exists an infinite, finitely presented, simple group. Graham -Higman gave the first example in 1951; a much shorter construction -appears in Higman's 1974 monograph *Finitely Presented Infinite Simple -Groups*. §122 in Knill's *Some Fundamental Theorems in Mathematics*. +There exists an infinite, finitely presented, simple group. The first +such examples come from Graham Higman's 1974 monograph *Finitely +Presented Infinite Simple Groups* — the Higman–Thompson groups +`G_{n, r}`. (Higman's 1951 paper had earlier exhibited a finitely +*generated* infinite simple group — a simple quotient of the +four-generator group with no nontrivial finite quotients — but did +not give a finite presentation for the simple quotient.) §122 in +Knill's *Some Fundamental Theorems in Mathematics*. Concretely: some `n` and a finite relator set `rels ⊆ FreeGroup (Fin n)` for which `PresentedGroup rels` is both simple and infinite. Pure existence of a pathological finite -presentation. Mathlib has `FreeGroup`, `PresentedGroup`, -`IsSimpleGroup`, and `Infinite`, but no construction of any infinite -finitely-presented simple group. +presentation. Mathlib v4.30 has `FreeGroup`, `PresentedGroup`, +`IsSimpleGroup`, `Infinite`, HNN extensions, and Britton's lemma, but +no Higman–Thompson construction and no infinite finitely-presented +simple group on hand. -/ /-- **Higman's infinite simple group** (G. Higman 1951/1974). There diff --git a/manifests/problems/higman_infinite_simple.toml b/manifests/problems/higman_infinite_simple.toml index aec4888..dd5e25c 100644 --- a/manifests/problems/higman_infinite_simple.toml +++ b/manifests/problems/higman_infinite_simple.toml @@ -4,6 +4,6 @@ test = false module = "LeanEval.GroupTheory.HigmanInfiniteSimple" holes = ["higman_infinite_simple"] submitter = "Kim Morrison" -notes = "There exists an infinite, finitely presented, simple group: some n and a finite relator set rels ⊆ FreeGroup (Fin n) for which PresentedGroup rels is both simple and infinite. Pure existence of a pathological finite presentation. Mathlib has FreeGroup, PresentedGroup, IsSimpleGroup, and Infinite, but no construction of any infinite finitely-presented simple group. §122 of Knill's *Some Fundamental Theorems in Mathematics*." +notes = "There exists an infinite, finitely presented, simple group: some n and a finite relator set rels ⊆ FreeGroup (Fin n) for which PresentedGroup rels is both simple and infinite. Pure existence of a pathological finite presentation. The first such examples come from Higman's 1974 monograph (the Higman–Thompson groups G_{n,r}); Higman's 1951 paper only constructs a finitely *generated* infinite simple group (a simple quotient of the four-generator group with no nontrivial finite quotients), not a finitely presented one. Mathlib v4.30 has FreeGroup, PresentedGroup, IsSimpleGroup, Infinite, HNN extensions (`Mathlib/GroupTheory/HNNExtension.lean`), and Britton's lemma, but no Higman–Thompson construction, no Higman embedding theorem, and no construction of an infinite finitely-presented simple group. §122 of Knill's *Some Fundamental Theorems in Mathematics*." source = "G. Higman, 'A finitely generated infinite simple group', J. London Math. Soc. 26 (1951) 61–64; G. Higman, *Finitely Presented Infinite Simple Groups*, Notes on Pure Mathematics 8, Australian National University, 1974. §122 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf)." -informal_solution = "Higman's 1951 group is built from four generators `a, b, c, d` with relations expressing that conjugation cycles through them as `b · a = a²·b`, `c · b = b²·c`, `d · c = c²·d`, `a · d = d²·a` — a `chain of squarings'. Higman proves (i) this group is finitely presented by construction; (ii) it is infinite by a combinatorial argument tracking the lengths of normal forms under the cyclic conjugation; (iii) it is simple by Britton's lemma applied to the HNN-extension decomposition implicit in the relators (any normal subgroup containing a nontrivial element must contain the whole group). The 1974 monograph gives a different, shorter construction via Higman's embedding theorem applied to a Boone–Higman simulation of a Turing machine with halting set inside the simple group. Mathlib has the substrate (`FreeGroup`, `PresentedGroup`, `IsSimpleGroup`, `Infinite`, normal closures via `Subgroup.IsNormalClosureFG`) but no HNN extensions, no Britton's lemma, no Higman embedding theorem, and no construction of an infinite finitely-presented simple group." +informal_solution = "Higman's 1974 monograph constructs the Higman–Thompson groups G_{n,r} (for integers n ≥ 2, r ≥ 1) as groups of piecewise-linear bijections of certain Cantor-like spaces / r-tuples of n-ary trees. Each G_{n,r} is finitely presented (explicit finite generators and relations are written down) and infinite by construction; the commutator subgroups G_{n,r}' (or G_{n,r} itself for suitable n, r) are simple, by an analysis of the action on the underlying space. Higman's 1951 paper had earlier exhibited a finitely *generated* infinite simple group — a simple quotient of the four-generator group `⟨a, b, c, d | bab⁻¹ = a², cbc⁻¹ = b², dcd⁻¹ = c², ada⁻¹ = d²⟩` with no nontrivial finite quotients — but did not give a finite presentation of the simple quotient. Mathlib v4.30 has the substrate (`FreeGroup`, `PresentedGroup`, `IsSimpleGroup`, `Infinite`, `Subgroup.IsNormalClosureFG`), HNN extensions and Britton's lemma (`Mathlib/GroupTheory/HNNExtension.lean`), but no Higman–Thompson groups, no Higman embedding theorem, and no construction of an infinite finitely-presented simple group."