{"id":"palomar/PALOMAR-2026-10-22-000010","url":"https://github.com/32805433/Universal-Group/tree/6416dd36ad22f3684583457f234519bafc851396","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000010-v1.json","repo":"https://github.com/32805433/Universal-Group","tags":["math.GR","group-theory","combinatorial-group-theory","lean"],"score":0,"title":"A universal group with thirteen relators","trust":"high","domain":"math.GR","source":"palomar","authors":["Qiuyu Ren"],"reviews":0,"subject":"math.GR","summary":"Lean 4 proof that there exists a presentation with two generators and thirteen relators whose group contains an isomorphic copy of every finitely presented group. The construction combines a universal finitely presented input, positive preparation, word recognition, a six-generator nineteen-relator host, and a final HNN compression.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Subgroups of finitely presented groups","identifier":"https://doi.org/10.1098/rspa.1961.0132","relationship":"adapts"},{"title":"Universal group with twenty-one defining relations","identifier":"https://doi.org/10.1016/0012-365X(77)90153-4","relationship":"adapts"},{"title":"Small undecidable groups and unrecognizable 4-manifolds","identifier":"https://arxiv.org/abs/2609.10461v1","relationship":"adapts"}]}