Residual finiteness of hyperbolic groups

The question of the residual finiteness of hyperbolic groups asks whether every word-hyperbolic group is residually finite, that is, whether every nonidentity element survives in some finite quotient. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 23 September 2026, claims a negative answer with a torsion-free example, and the collection includes a Lean formalization of that statement. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of the manuscript:
  • The question belongs to the programme initiated by Gromov's theory of hyperbolic groups and appears among the standard open problems of the area (for example Problem (H1) in the list of Baumslag, Myasnikov and Shpilrain, and Question 1.15 in Bestvina's list).
  • Ilya Kapovich and Wise proved that all hyperbolic groups are residually finite if and only if every nontrivial hyperbolic group has a nontrivial finite quotient, and if and only if every hyperbolic group is virtually torsion-free. Agol, Groves and Manning proved that a positive answer would make every quasiconvex subgroup of every hyperbolic group separable.
  • Additional structure forces residual finiteness: by the work of Haglund and Wise and Agol's theorem, a hyperbolic group acting properly and cocompactly on a CAT(0) cube complex is virtually special and hence linear. Without hyperbolicity, Wise's complete square complexes and the Burger–Mozes groups show that nonpositive curvature is compatible with the failure of residual finiteness.

The original result

• Claim. Theorem 1.1 of A torsion-free hyperbolic group that is not residually finite states that there exists a torsion-free word-hyperbolic group that is not residually finite. The group is the fundamental group of a finite Euclidean triangle complex, and a member of a fixed finite family of nontrivial elements belongs to the finite residual, the intersection of the kernels of all homomorphisms to finite groups; the argument does not identify which member.
• Consequence stated in the manuscript. Corollary 1.2 states that one fixed nonidentity element is killed by every finite-dimensional linear representation of the group over every commutative field, so that the group is not linear over any commutative field. The manuscript notes that nonlinear hyperbolic groups were already known (Michael Kapovich; Tholozan and Tsouvalas).
• Method, as described:
  • Affine lines over a large prime field, each with a marked point, give an incidence graph of large girth; each line label contributes an array of edges between two vertices of the complex, and a four-edge loop from two rows and two columns of an array gives a nontrivial "rectangular word".
  • If all rectangular words survived in a finite quotient, the edge arrays in its regular permutation representation would have large real rank, which a determinant argument keeps over the fixed prime field; product Lagrange interpolation at the marked points gives a tensor identity whose other side has small rank.
  • Torsion-freeness and hyperbolicity come from a triangle-complex criterion on angular lengths of closed walks in vertex links, proved through reduced planar diagrams and an angular Gauss–Bonnet argument.
• Source. The manuscript A torsion-free hyperbolic group that is not residually finite at commit 1581d4c.
• Formalization. The repository's scope note links the Comparator statement TorsionFreeHyperbolic.lean, whose theorem states the existence of a torsion-free word-hyperbolic group that is not residually finite, with word-hyperbolicity defined by uniformly thin geodesic triangles in a Cayley graph. The scope note states that nonlinearity over every field is not a separate conclusion of the linked statement.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 19–20 October 2026)
2026-10-07	S. Douglas, N. Mghirbi, Non-soficity of OpenAI's torsion-free hyperbolic group (Zenodo 10.5281/zenodo.23202474, all versions; Apsiape/hyperbolic-group-not-sofic at commit a4cb844)	Extension (with Lean)	Theorem 1.1 states that the manuscript's group is not sofic. The authors describe the idea as follows: the rank argument uses a finite quotient only through its permutation matrices, and it survives approximation, so approximate permutation models are excluded at a fixed positive accuracy. Corollary 1.3 states that one fixed rectangular word lies in the kernel of every homomorphism to a sofic group. The README states that the Lean theorem Approx252.exists_torsionFree_wordHyperbolic_not_sofic, built on OpenAI's development, asserts the existence of a torsion-free word-hyperbolic group that is not sofic, with a standard definition of soficity (normalized Hamming distance) written in the repository, and uses only the standard axioms; it publishes the authors' rebuild logs. Sharper constants, the corollaries and the results added in version 1.1.0 are proved in writing only. Version 1.1.0 (14 October 2026) adds a theorem that for every division ring of the characteristic fixed by the construction, the group ring of any group containing the group has no Linnell division ring, together with structural results (a free-product splitting, failure of bi-orderability). The note states that the work was developed with AI models from more than one developer and that the group and every input to the non-soficity argument are OpenAI's.	Zenodo record (version 1.0.0 on 7 October, version 1.1.0 on 14 October 2026); GitHub repository.
2026-10-08	Formal Conjectures pull request #6921 (HyperbolicGroupsResiduallyFinite.lean at commit 7db2ea3)	Statement	Marks Problem (H1)(a) (residual finiteness of hyperbolic groups) and Problem (H1)(b) (a proper finite-index subgroup in every nontrivial hyperbolic group) as solved with a negative answer, citing the manuscript; the second follows through the Kapovich–Wise equivalence stated in the same file. The docstring links the collection's Lean proof and notes that its definition of hyperbolicity is equivalent to the library's, but that the equivalence is not part of that proof. The pull request notes that neither theorem has a formal-proof link.	Merged; later commits on 14 October 2026 changed only repository-wide annotations.
2026-10-08	MathVet (GitHub; review of openai/math at commit adc7f12, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates this family "full" and records a sandboxed Comparator pass for the challenge TorsionFreeHyperbolic. Its note states that the nonlinearity claim is not separately stated in Lean and follows from non-residual-finiteness by Malcev's theorem.	The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
2026-10-13	H. Sandhu, A. Thom, An example of a non-sofic hyperbolic group (note on A. Thom's web page; arXiv:2610.24836v1)	Extension (independent construction)	Theorem A states that there is a finite connected two-dimensional triangle complex with a locally CAT(−1) metric whose fundamental group is torsion-free, word-hyperbolic and not sofic. In place of a random incidence graph, the construction uses the explicit Lazebnik–Ustimenko graph D(5, q) for a fixed prime q. Corollary B states that there is a nontrivial torsion-free word-hyperbolic group with no nontrivial sofic quotient, by the theorem of Kapovich and Wise applied to the class of sofic groups. The note also observes that the group admits no proper cocompact action on a CAT(0) cube complex. The note states that it builds on the manuscript, from which it uses the marked lines, the triangle relations built from Cartesian products, the interpolation identity and the comparison of real and finite-field ranks. Its acknowledgments state that it is based on an AI-generated construction obtained by H. Sandhu on 7 October 2026, and that it cites the work of Douglas and Mghirbi as an independent AI-assisted proof.	Note in PDF form on the author's web page (file dated 13 October 2026); posted to arXiv as version 1 of 17 October 2026, whose abstract states that the construction builds on OpenAI's construction of a non-residually finite hyperbolic group.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
• Related pages on OpenAI's torsion-free groups cited in version 1.1.0 of the note of Douglas and Mghirbi: Kaplansky's zero-divisor conjecture, Kaplansky's direct-finiteness conjecture.