diff --git a/LeanEval/GroupTheory/HigmanInfiniteSimple.lean b/LeanEval/GroupTheory/HigmanInfiniteSimple.lean
new file mode 100644
index 0000000..75df9f2
--- /dev/null
+++ b/LeanEval/GroupTheory/HigmanInfiniteSimple.lean
@@ -0,0 +1,40 @@
+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. 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 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
+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..dd5e25c
--- /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. 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 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."