Kuznetsov's theorem: finitely presented simple groups have solvable word problem

boone_higman_simple

Submitter: Kim Morrison.

Notes: A finitely presented *simple* group has a decidable word problem. The word problem of a finite presentation φ : FreeGroup (Fin n) →* G is encoded as the predicate `w ↦ φ (FreeGroup.mk w) = 1' on `List (Fin n × Bool)' (signed-letter words); solvability is `ComputablePred' of that predicate — genuine algorithmic decidability via a Turing machine, not a bundled Prop. The hypotheses `hsurj` + `hker` unpack `Group.IsFinitelyPresented G` for this presentation. Solvability of the word problem is independent of the chosen finite presentation, so quantifying over an arbitrary one is the standard reading. §122 of Knill's *Some Fundamental Theorems in Mathematics*.

Source: A.V. Kuznetsov, 'Algorithms as operations in algebraic systems', Uspekhi Mat. Nauk 13 (1958) 240–241 (Russian); W.W. Boone and G. Higman, 'An algebraic characterization of groups with soluble word problem', J. Austral. Math. Soc. 18 (1974) 41–53. §122 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Kuznetsov's argument is r.e.-from-both-sides. (1) The set of words `w' with `φ(w) = 1' is recursively enumerable: enumerate the relators and all of their formal consequences (conjugates, products, and inverses). (2) For a nontrivial simple group G, the *negation* `φ(w) ≠ 1' is also r.e.: if `w' is nontrivial in G, the normal closure of `w' is all of G, so adding `w = 1' as a relator collapses the presented group to the trivial group. Concretely, semi-decide `w ≠ 1' by enumerating consequences of `rels ∪ {w}' until each generator g_i is forced to equal 1; once that finite generator-collapse certificate appears, `w ≠ 1' is confirmed. (3) Both r.e. ⇒ decidable (the standard `r.e. ∧ co-r.e. ⇒ decidable' theorem). The lean-eval `IsSimpleGroup' typeclass extends `Nontrivial', so the trivial-group degeneracy is excluded automatically. Mathlib has `Group.IsFinitelyPresented', `Subgroup.IsNormalClosureFG', `FreeGroup', `PresentedGroup', `IsSimpleGroup', and the `ComputablePred` / `Computable` / `Partrec` stack, but no notion of a word problem, no Kuznetsov / Novikov result, and no r.e./co-r.e. machinery wired to group presentations.

theorem declaration uses `sorry`boone_higman_simple {G : Type*} [Group G] [IsSimpleGroup G]
    {n : ℕ} (φ : FreeGroup (Fin n) →* G)
    (_hsurj : Function.Surjective φ)
    (_hker : (MonoidHom.ker φ).IsNormalClosureFG) :
    LeanEval.GroupTheory.BooneHigmanSimpleProblem.WordProblemSolvable φ := byG:Type u_1inst✝¹:Group Ginst✝:IsSimpleGroup Gn:ℕφ:FreeGroup (Fin n) →* G_hsurj:Function.Surjective ⇑φ_hker:φ.ker.IsNormalClosureFG⊢ WordProblemSolvable φ
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 3, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on Jun 3, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 4, 2026