A 3-generator 9-relator group with unsolvable word problem, and smaller Adian-Rabin families
A group given by 3 generators and 9 relations has an unsolvable word problem, beating the 12-relation record Borisov set in 1969, and it yields families of 4-generator 11-relator and 2-generator 10-relator presentations for which no algorithm can decide whether the group is trivial.
- Lab
- Independent
- Model
- GPT-5.6 Sol Pro (construction); GPT-5.6 Sol in Codex (Lean formalization)
- Field
- Mathematics
- Date
- 2026-09-09
- Human collaborators
- Marc Kegel, Shana Yunsheng Li, Qiuyu Ren
What was found
How small a finite presentation can be while still being algorithmically undecidable is a quantitative question that runs from Boone's 32-relator group through Collins to Borisov's 12. Starting from Borisov's group, the construction adds two HNN extensions and then removes seven redundant relators and six generator-relator pairs by Tietze transformations, leaving 3 generators and 9 relators. Feeding that group into Tancer's and Gordon's reductions, with two further Tietze eliminations in Tancer's case, gives the two Adian-Rabin families, improving Tancer's deficiency-9 family and Gordon's 13-relator family. By Markov's argument these give Corollary 1.5, that a connected sum of n copies of S2 x S2 is topologically unrecognizable for n at least 7 and smoothly unrecognizable for n at least 9. The three algebraic theorems, with every dependency down to Post's machine-to-Thue construction and Matiyasevich's three-rule Thue system, are formalized in about 28,000 lines of Lean.
Novelty check
The paper fixes the prior state of the art by name: Borisov 1969 at 12 relators for the word problem, Tancer 2023 at deficiency 9 and Gordon 2022 at 13 relators for Adian-Rabin families, which gave topological unrecognizability of 9 copies and smooth unrecognizability of 12 copies of S2 x S2. The registry was searched on 2026-09-24 for Adian, Rabin, unrecognizable, word problem and 4-manifold with no hits, and a web search for recent fewest-relator results turned up only this paper and Tancer's 2023 preprint. Of the four registries the watch reads, only Palomar holds a record, and it is the authors' own formalization of this paper. The paper itself records a competing result in progress: Cameron Gordon has independently improved the smallest Adian-Rabin families along similar lines and obtained both smooth and topological unrecognizability of 8 copies, in a paper not yet out. That will leave the topological bound of 7 here as the stronger one, but will supersede the smooth bound of 9. The problem has no single origin year, so year_posed is left unrecorded.
Caveats and known objections
Graded author verified rather than formal even though the three algebraic theorems carry a Lean proof registered on Palomar. The four-manifold corollary, which the paper's title leads with, is a conventional argument on top of the formalized algebra and is not machine-checked, as Palomar's own record says. The Lean statements were checked only by the authors: the Lean comparator accepts the proof and the axiom audit reports only the three standard principles, but no third party has audited the statements against the paper, and a Palomar registration establishes that the proof typechecks against the recorded statement, not that the statement is the paper's theorem. Autonomy is graded ai-led on an explicit disclosure in section 1.5: the main construction was essentially developed by GPT-5.6 Sol Pro, which proposed the two HNN extensions, the Tietze reductions and the two extra eliminations behind Theorem 1.3, while the authors independently checked and reorganized the arguments, verified the references and take responsibility for correctness. It is not autonomous because the authors chose the problem and directed the work. The model also flagged two corrections needed in Tancer's 2023 paper, which Tancer confirmed to the authors, and the reduction behind Theorem 1.3 uses the corrected form. An unrefereed preprint at entry.
Machine-checked elsewhere
PalomarPALOMAR-2026-09-22-000002
32805433/Adian-Rabin at fb4a401e8fbd · checked 2026-09-22
ProvedUndecidability.exists_three_generator_nine_relator_group_with_unsolvable_word_problemUndecidability.exists_four_generator_eleven_relator_adian_rabin_familyUndecidability.exists_two_generator_ten_relator_adian_rabin_family
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Registered by the paper's own authors. These are Theorems 1.1, 1.3 and 1.4; the record states that the four-manifold consequences are outside the formalized scope.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Author verified and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded author verified for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). A 3-generator 9-relator group with unsolvable word problem, and smaller Adian-Rabin families. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-09-small-undecidable-groupsBibTeX
@misc{whataifound-independent-2026-groups,
title = {A 3-generator 9-relator group with unsolvable word problem, and smaller Adian-Rabin families},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Author verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-09-09-small-undecidable-groups}
}