{"id":"palomar/PALOMAR-2026-09-22-000002","url":"https://github.com/32805433/Adian-Rabin/tree/fb4a401e8fbdba36e7b35c11fde2baa15592e185","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-22-000002-v1.json","repo":"https://github.com/32805433/Adian-Rabin","tags":["math.GR","math.LO","msc:20F10","msc:20F05","msc:03D35","group-theory","undecidability","word-problem","lean"],"score":0,"title":"Small undecidable groups and fixed-size Adian–Rabin families","trust":"high","domain":"math.GR","source":"palomar","authors":["Marc Kegel","Shana Yunsheng Li","Qiuyu Ren"],"reviews":0,"subject":"math.GR","summary":"Lean 4 proofs of the algebraic results in Small undecidable groups and unrecognizable 4-manifolds (arXiv:2609.10461v1): existence of a group with a three-generator, nine-relator presentation and unsolvable word problem; an effective family of four-generator, eleven-relator presentations with undecidable triviality; and an effective family of two-generator, ten-relator presentations with undecidable triviality. These are Theorems 1.1, 1.3, and 1.4 of the paper. The four-manifold consequences in the paper are outside the formalized scope.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-22","reactions":{},"formalized":true,"formalizes":[{"title":"Small undecidable groups and unrecognizable 4-manifolds","identifier":"https://arxiv.org/abs/2609.10461v1","relationship":"formalizes"},{"title":"Simple examples of groups with unsolvable word problem","identifier":"https://doi.org/10.1007/BF01101402","relationship":"adapts"},{"title":"Word problem for Thue systems with a few relations","identifier":"https://doi.org/10.1007/3-540-59340-3_4","relationship":"adapts"},{"title":"Recursive unsolvability of a problem of Thue","identifier":"https://doi.org/10.2307/2267170","relationship":"adapts"},{"title":"Decision problems for groups—survey and reflections","identifier":"https://doi.org/10.1007/978-1-4613-9730-4_1","relationship":"adapts"}]}