Constructs a torsion-free word-hyperbolic group that is not residually finite, answering the residual-finiteness question negatively. One fixed nonidentity element is killed by every finite-dimensional linear representation over every commutative field, so the group is not linear over any such field. (Lean)
Manuscript
A torsion-free hyperbolic group that is not residually finite
September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:a-torsion-free-hyperbolic-group-that-is-not-residually-finite-September-23-2026}
We construct a torsion-free word-hyperbolic group that is not residually finite, answering the residual-finiteness question for hyperbolic groups negatively.
Result 252 · Group theory. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md