Open Research Index

Small undecidable groups and fixed-size Adian–Rabin families

Marc Kegel, Shana Yunsheng Li, Qiuyu Ren

Palomar Registrypalomar/PALOMAR-2026-09-22-000002Sep 22, 2026math.GRscore 0

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.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-22-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-22-000002/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-22-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'