finite.works
Results · Groups and their finite shadows

Non-soficity of OpenAI’s torsion-free hyperbolic group

Seth Douglas and Nidhal Mghirbi · version 1.1.0 · Zenodo, · doi:10.5281/zenodo.23374284 · PDF

In plain wordsA recently built torsion-free hyperbolic group, made so that its finite quotients cannot see all of it, cannot be imitated by permutations either: approximate models fail at a fixed accuracy, so the group is not sofic, and one fixed element dies in every sofic quotient.

The result

As the paper states it, in briefOpenAI’s torsion-free word-hyperbolic group, built not to be residually finite, is not sofic: its rank argument survives approximation. Version 1.1.0 adds that its group rings over division rings of the construction’s characteristic have no Linnell division ring.

Questionson the index

How this was checked

Lean
The headline, that a torsion-free word-hyperbolic group is not sofic, is formalized in Lean 4 on OpenAI’s development, with standard axioms only. Sharper constants and the version 1.1.0 results are proved in writing.
Peer review
Not yet.

Every check here is internal. How we check results.

Label checked .

Novelty and credit

Novelty
The group and every input to the argument are OpenAI’s; the approximate argument, its constants and the formalization are ours. Cites Chapman and Peled’s conditional construction and the independent note of Thom based on Sandhu’s construction.

Versionsthree, each with its own DOI

Every archived version, newest first. Dates are Zenodo publication dates. All versions: 10.5281/zenodo.23202474, which always resolves to the newest.
VersionDateDOINotes
1.1.010.5281/zenodo.23374284Correction: Alongside new results: the note of Sandhu and Thom is described correctly and credited with its authors; Ivanov (arXiv:2610.17662) is credited for torsion-free zero divisors in odd characteristic; credit added for Ozawa and Pestov, Kun, Kun and Thom, Elek and Szabó, Alon, Hall, Knauer, Pinchasi and Yuster, and others; a corollary now states only its new part. The non-soficity argument is unchanged. PDF hosted here.
1.0.110.5281/zenodo.23345877Correction: Incomplete credit in version 1.0.0. Version 1.0.1 cites Chapman and Peled’s conditional construction, Soulé’s torsion bound and Thom’s independent note based on Sandhu’s construction. No mathematical change.
1.0.010.5281/zenodo.23202475

Paper, code and links

PDF

papers/non-sofic-v1.1.0.pdf, version 1.1.0, 619,315 bytes.

SHA-256 2c30dc563fb4782a14c230ee640288f15482b05940dc40f8e4a0831ea39ef8cf

Corrections

  1. Version 1.1.0. Alongside new results: the note of Sandhu and Thom is described correctly and credited with its authors; Ivanov (arXiv:2610.17662) is credited for torsion-free zero divisors in odd characteristic; credit added for Ozawa and Pestov, Kun, Kun and Thom, Elek and Szabó, Alon, Hall, Knauer, Pinchasi and Yuster, and others; a corollary now states only its new part. The non-soficity argument is unchanged.doi:10.5281/zenodo.23374284
  2. Version 1.0.1. Incomplete credit in version 1.0.0. Version 1.0.1 cites Chapman and Peled’s conditional construction, Soulé’s torsion bound and Thom’s independent note based on Sandhu’s construction. No mathematical change.doi:10.5281/zenodo.23345877

All corrections, and what counts as one.

Cite

@misc{douglas2026nonsofic,
  author  = {Douglas, Seth and Mghirbi, Nidhal},
  title   = {Non-soficity of {OpenAI}'s torsion-free hyperbolic group},
  year    = {2026},
  version = {1.1.0},
  doi     = {10.5281/zenodo.23374284},
  url     = {https://doi.org/10.5281/zenodo.23374284}
}

non-sofic.bibAll papers as BibTeX