# A torsion-free hyperbolic group that is neither residually finite nor linear over any field

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A torsion-free hyperbolic group that is not residually finite](../../preprints/a-torsion-free-hyperbolic-group-that-is-not-residually-finite-September-23-2026/paper.pdf)

## Scope

The residual-finiteness question for hyperbolic groups asks whether every nonidentity element survives in some finite quotient. The formalized result gives a negative answer by constructing a torsion-free word-hyperbolic group that is not residually finite.

Nonlinearity over every field is not a separate conclusion of the statement linked below.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Torsion-free hyperbolic group that is not residually finite | [TorsionFreeHyperbolic.lean](../ComparatorChallenges/TorsionFreeHyperbolic.lean) |