Curved, yet hidden from finite shadows?
An AI preprint claims a torsion-free hyperbolic group that is not residually finite
Covers result 252 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
5:08. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
A finite quotient of a group is a shadow of it in a finite group, the way the integers cast a shadow on a twelve-hour clock. A group is residually finite if every element other than the identity survives in some shadow. Hyperbolic groups, whose geodesic triangles are uniformly thin, were guessed by Gromov in 1987 to be probably not residually finite in general. Yet no example was known, and many cases, such as groups acting nicely on cube complexes, turned out to be residually finite after all. Kapovich and Wise, and independently Olshanskii, showed that a single counterexample would mean some hyperbolic group has no finite quotients at all. By Malcev’s theorem, finitely generated matrix groups over a field are residually finite.
Result 252 is one OpenAI preprint, 21 pages, dated September 23, 2026. It claims a torsion-free hyperbolic group that is not residually finite: one fixed element other than the identity dies in every finite quotient. By Malcev, that element also dies in every finite-dimensional representation over every commutative field, so the group is not linear.
What it doesn’t claim
An explicit group or element. The group is chosen at random, and the dying element is one member of a finite list, unidentified. It is enormous: from the paper’s constraints, the prime needs at least 125 digits and the presentation has more than 102580 generators. It is also not the first group of nonpositive curvature that fails to be residually finite. Wise, and Burger and Mozes, had such groups, but theirs were not hyperbolic.
Where it stands
- Posted as a preprint
- OpenAI, 21 pages, dated September 23, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- The main theorem (docs)
Last checked October 19, 2026. The preprint has not been revised. In Lean, the main theorem is formalized: about 10,700 lines with no unproved steps. We did not build it, but an outside group reports rebuilding it. The nonlinearity corollary is not formalized, and OSVerify has not reviewed the paper. On MathOverflow, Ian Agol wrote that he read the preprint and that it looks correct to him. He also noted what seem to be uncited results in combinatorics behind the methods. Within a week of the public release, two AI-assisted follow-ups reused the rank count to show that a hyperbolic group need not even be sofic, and that this one is not.
How the proof goes
- A random, curved complex. Scatter random lines through a 20-dimensional space over a finite field and delete the few that lie on short cycles. From the incidences, build a complex with three vertices and triangles whose angles are 108°, 36° and 36°. Around every vertex, the angles along any loop add up to more than 360°. So the group is hyperbolic and torsion-free, and every rectangle (two rows by two columns of one grid of edges) is not the identity.
- Ranks in any finite shadow. In a finite quotient where all rectangles survive, turn each edge into a permutation matrix. Surviving rectangles force each grid to have high rank. The triangle relations force the sums of those grids to have low rank.
- The equation that cannot hold. An interpolation identity over the finite field glues the two into one impossible equation, whatever the size of the quotient. The prime is fixed in advance, and Hadamard’s inequality keeps the rank from collapsing modulo the prime. Since there are only finitely many rectangles, one fixed rectangle dies in every finite quotient.
The numbers in the video
- Ours: in a Baumslag–Solitar group, the commutator [tat⁻¹, a] is not the identity, yet it vanished in all 16,833 maps to permutation groups on up to 7 points.
- Ours: a measured thinness constant grows 1, 2, 3, 4, 5 in the plane and stays 0 in the free group.
- Ours: Sanov’s matrices reduced modulo primes caught every sample word; one first showed up modulo 13.
- Ours: with permutations of 5 points, an array with every rectangle alive had rank 472 of 480. An array built to factor had rank 120, and every rectangle in it was dead.
Read the source
- A torsion-free hyperbolic group that is not residually finite (PDF), 21 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 252.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
A finite quotient of a group is a shadow of it in a finite group, the way the integers cast a shadow on a 12-hour clock. A group is residually finite if every element other than the identity survives in some shadow. Free groups are: our computer caught each of 11 sample words with permutations of at most 4 points. But a Baumslag–Solitar group has a commutator that is not the identity, yet it vanished in all 16,833 maps to permutation groups on up to 7 points. That group is far from negatively curved. Hyperbolic groups are: their geodesic triangles are uniformly thin. Our computer measured a thinness constant: in the flat plane it grows, 1, 2, 3, 4, 5, as the region grows; in the free group, a tree, it stays at zero. In 1987 Gromov guessed that generic hyperbolic groups are probably not residually finite, but no one could build even one, and many cases, like those acting nicely on cube complexes, turned out residually finite after all. The question matters. Kapovich and Wise, and independently Olshanskii, showed that if every nontrivial hyperbolic group has even one finite quotient, then every hyperbolic group is residually finite. So a single counterexample means some hyperbolic group has no finite quotients at all. And residual finiteness is tied to linearity: by Malcev, a finitely generated group of matrices over a field is residually finite. Our computer reduced matrices modulo primes and caught every sample word; one first showed up modulo 13.
1:44The claim
Result 252 is one OpenAI preprint, 21 pages, dated September 23, 2026. It claims a torsion-free hyperbolic group that is not residually finite: one fixed element other than the identity dies in every finite quotient. By Malcev, that element also dies in every finite-dimensional representation over every commutative field, so the group is not linear. Not claimed: an explicit group or element. The group is chosen at random, and the dying element is one member of a finite list, unidentified. It is enormous: from the paper’s constraints, the prime needs at least 125 digits, and the presentation has more than 10²⁵⁸⁰ generators. And it is not the first non-residually-finite group of nonpositive curvature; Wise and Burger and Mozes had those, but they were not hyperbolic.
2:42How the proof goes
The construction: scatter random lines through a 20-dimensional space over a finite field, and delete the few on short cycles. From the incidences build a complex with three vertices and triangles with angles of 108°, 36° and 36°. Around every vertex, the angles along any loop add up to more than 360°, so the group is hyperbolic and torsion-free, and every rectangle, two rows by two columns of one grid of edges, is not the identity. Now take any finite quotient where all rectangles survive, and turn each edge into a permutation matrix. Surviving rectangles force the matrices of each grid to have high rank. But the triangle relations force their sums to have low rank. Our toy, with permutations of 5 points: an array with every rectangle alive has rank 472 out of 480; an array built to factor has rank only 120, and every rectangle dies. An interpolation identity over the finite field glues the high-rank pieces and the low-rank sums into one equation that cannot hold, whatever the size of the finite quotient. The prime must be chosen before the quotient is known; a determinant inequality of Hadamard keeps the rank from collapsing modulo the prime. Since there are only finitely many rectangles, one fixed rectangle must die in every finite quotient.
4:12Where it stands
The preprint is unrefereed and unchanged since release. In Lean, the main theorem is formalized, about 10,700 lines with no unproved steps; we did not build it, but an outside group reports rebuilding it. The nonlinearity corollary is not formalized. OSVerify has not reviewed it. On MathOverflow, Ian Agol wrote that he read the preprint and it looks correct to him, noting what seem to be uncited results in combinatorics behind the methods. Within a week of the public release, two follow-ups, also AI-assisted, reused the rank count to show that a hyperbolic group need not even be sofic, this one included. If it holds, curvature does not guarantee finite pictures: a hyperbolic group can hide an element from every finite shadow, 39 years after Gromov guessed it.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.