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

Is every word-hyperbolic group sofic? This was an open question. OpenAI recently constructed a torsion-free word-hyperbolic group G that is not residually finite, and formalized that theorem in Lean. We show that G is not sofic. Their rank argument against finite quotients uses a finite quotient only through its permutation matrices, and it survives approximation: a relation that holds on all but a small fraction of points costs a small rank error, and a word with few fixed points costs a small trace error. The argument therefore excludes approximate permutation models at a fixed positive accuracy, while soficity would provide such models at every accuracy. Moreover, one fixed nonidentity element of G dies under every homomorphism from G to a sofic group, and G is neither LEF nor residually amenable. The group and every input to the argument are OpenAI's. Our contribution is the approximate rank argument, with explicit constants, and a Lean formalization of its conclusion on top of OpenAI's development: some torsion-free word-hyperbolic group is not sofic.