Sandhu and Thom build one from OpenAI’s non-residually-finite hyperbolic group, starting from an AI-generated construction; Douglas–Mghirbi give an independent AI-assisted proof with Lean

Your AI and this story

Key facts

• Paper: ‘An example of a non-sofic hyperbolic group’, Harjas Sandhu and Andreas Thom, arXiv 2610.24836 [math.GR], 17 Oct 2026. Abstract: ‘We construct a torsion-free, two-dimensional, word-hyperbolic group which is not sofic. Our construction builds on OpenAI’s construction of a non-residually finite hyperbolic group [14].’
• Background (paper): ‘The question whether all groups are sofic was open for a long time. The first proof of the existence of a non-sofic group was given by OpenAI’ (Astra’s ‘Nonsofic groups exist’, Ten Advances, Aug 2026). Kun and Thom built non-sofic wreath products; Chapman and Peled gave a conditional non-sofic hyperbolic group from random simplicial complexes (arXiv 2509.21566)
• Construction: fundamental group of a triangle complex with a locally CAT(−1) metric, built from marked lines in D(5, q) over F_q^5, with real versus finite-field rank comparison; Ian Agol pointed to Dvir’s finite-field Kakeya work for the interpolation step (Lemma 2.1)
• Acknowledgments, verbatim: ‘This paper is based on an AI-generated construction obtained by Harjas Sandhu on October 7, 2026, which was in turn based on the OpenAI breakthrough [14]. The second author worked through the proof to make it readable and to reduce unnecessary overhead. OpenAI’s GPT Astra helped draft this document. … An independent AI-assisted proof was given by Douglas–Mghirbi [5].’ They ‘view this document as a commentary on OpenAI 252’
• Douglas–Mghirbi, ‘Non-soficity of OpenAI’s torsion-free hyperbolic group’ (GitHub Apsiape/hyperbolic-group-not-sofic, created 7 Oct 2026, Zenodo DOI 10.5281/zenodo.23202474): OpenAI’s rank argument against finite quotients ‘survives approximation’, so the same group is not sofic. ‘The group and every input to the argument are OpenAI’s; the approximate argument, its constants and the formalization are ours.’ The Lean code builds on OpenAI’s development
• Douglas–Mghirbi v1.1.0 adds: for division rings K of the construction’s characteristic q, K[G] has no Linnell division ring; G is not bi-orderable
• Context: in September Thom argued that OpenAI’s August non-sofic result relied on his 2019 work with Kun (see the Astra ten-advances entry). Here he is co-author of a paper building on OpenAI’s later construction
• Dependency: OpenAI family 252, ‘A torsion-free hyperbolic group that is not residually finite’, is an unrefereed manuscript from the 6 Oct release (Lean-formalized according to OpenAI’s catalogue). Whether every hyperbolic group is residually finite is itself a famous open question (Gromov)