Small undecidable groups and unrecognizable 4-manifolds
Marc Kegel, Shana Yunsheng Li, Qiuyu Ren
math.GR
Sep 9, 2026 · v1
math.GT
TL;DR
A Lean 4 formalization machine-checks the algebraic results about the constructed small group with unsolvable word problem.
Abstract
We construct a $3$-generator $9$-relator group with unsolvable word problem. We use the group to construct two fixed-size Adian–Rabin families of group presentations, one with $4$ generators and $11$ relators, and another with $2$ generators and $10$ relators. As a consequence, $\#_7(S^2\times S^2)$ is topologically unrecognizable and $\#_9(S^2\times S^2)$ is smoothly unrecognizable. These algebraic and topological results improve the previous best known bounds by Borisov, Tancer, and Gordon. The construction of the group builds upon an example of Borisov and uses additional HNN extensions and Tietze eliminations to reduce the size of the presentation. We also provide a machine-checked Lean 4 formalization of the algebraic results.
Problem
How small can a finite group presentation be while still exhibiting algorithmically undecidable behavior, such as an unsolvable word problem or membership in an Adian–Rabin family? Previous smallest known example had 12 relators.
Approach
Starting from a finitely presented semigroup obtained via Matiyasevich's construction, the authors build a sequence of groups using HNN extensions, following and extending an example of Borisov. Tietze eliminations are applied to reduce the number of generators and relators. The resulting algebraic facts are formalized and machine-checked in Lean 4.
Results
They construct a 3-generator 9-relator group with unsolvable word problem, and Adian–Rabin families with 4 generators/11 relators and 2 generators/10 relators. Consequently #_7(S^2×S^2) is topologically unrecognizable and #_9(S^2×S^2) is smoothly unrecognizable, improving prior bounds.
