News · 2026-08-01

The non-sofic group is the one OpenAI claim a computer can check

OpenAI's new manuscript claims to have constructed a non-sofic group - settling a question group theorists have left open for decades - and released roughly 34,000 lines of Lean code so anyone can machine-check the argument. The claim is that the unit group of the binary Leavitt algebra cannot be approximated by finite permutation groups. No working group theorist has publicly endorsed or refuted it yet.

Key facts

• The claim: the unit group of the binary Leavitt algebra is not sofic, and a finitely presented non-sofic group therefore exists.
• GitHub lists the released NonSoficGroup.lean file at roughly 34,000 lines, with no sorry or axiom placeholders and build instructions for Lean 4.32.0 with Mathlib.
• Published 1 August 2026 as Chapter 3 of OpenAI's ten-result collection. It is not on arXiv.
• Primary source: the ten-proofs repository and the Lean source file.

Of the ten claims in OpenAI's release, this is the one worth following, because it is the one that is cleanly falsifiable. It is a single yes-or-no question with a decades-long history, a named object, and a published machine-readable proof.

Start with what soficity means, because the viral explanations have it badly wrong. Imagine trying to imitate an infinite group - an infinite set of symmetries with a multiplication rule - using nothing but shuffles of a finite deck of cards. You pick a handful of elements, find permutations of a big finite set that multiply almost the way those elements do, and let the error shrink as the deck grows. If that is always possible, the group is sofic. Every group anyone had ever constructed turned out to be sofic. Whether a non-sofic group existed at all had been open since the question was posed.

OpenAI's candidate is not a vague pathological object. It is the unit group of the binary Leavitt algebra, an algebra with the strange self-similarity property that one copy of a module looks like two copies of itself - the algebraic version of a shape that contains a full-size replica of itself inside a corner.

The proof is a contradiction with a sharp bottleneck. Assume the group has a sofic approximation. Property-(T) subgroups then convert those finite approximations into a collection of expander graphs, which are sparse networks that are nonetheless very hard to cut in two. Separately, the algebra contains a disjoint copy of Thompson's group V, an object that is infinite, simple, and finitely presented. A known theorem of Kun and Thom says that if you can isolate a single expanding component that still carries the V action, V would have to be locally embeddable into finite groups - and a finitely presented group with that property is residually finite, which an infinite simple group cannot be. Contradiction.

The genuinely new step, the one that will decide whether this holds, is item four in that chain: getting from many expanders to one. The manuscript uses two self-similar compressions and a bounded median-of-component-sizes argument to isolate the single component the Kun-Thom obstruction needs. Everything else in the proof is assembled from known results. That single lemma is where an outside referee will look first.

One nuance is already being overstated online. The manuscript proves a specific elementary group is non-sofic, then derives from a finite obstruction that some infinite finitely presented non-sofic group exists. It does not hand you an explicit finite presentation for that group. Phrasing that says OpenAI "supplied a finitely presented example" is stronger than what is on the page. The manuscript is also explicit about two things it does not do: it does not establish a non-hyperlinear group, and it does not settle the remaining positive-characteristic cases of Kaplansky-style finiteness conjectures.

The formalization is what makes this checkable rather than merely announced. The released Lean file's top-level theorem states non-soficity of a specific binary-Leavitt elementary group and then the existence of a finitely presented non-sofic group. Its manifest reports only Lean's standard foundational axioms and no unproved placeholders. That is a much stronger artifact than a proof sketch on a preprint server.

It is still not verification. Nobody outside OpenAI has publicly compiled the repository, and nobody has publicly audited whether the formal definitions - of soficity, of the Leavitt algebra, of the group - match the mathematical objects the prose describes. That audit is the whole ballgame, and it is the reason the responsible status today is "publicly inspectable and formally checkable, externally unreviewed."

The honest caveat is about scope. Non-soficity is a statement about approximating a group by finite permutations. It is not a limit on statistical learning, not a limit on compression, not a limit on quantum computing, and not evidence that AI has hit or broken through any ceiling. It is a beautiful, narrow, long-awaited answer to a specific algebraic question - and it happens to have arrived with a corporate author, a proof assistant, and no human name on it.

A separate thread should not be fused into this one: Fields Medallist Jacob Tsimerman has confirmed he is taking leave to join OpenAI, and has said the work is on AI safety rather than capabilities. Nothing in the manuscript identifies him as an author, contributor, or verifier.

Primary source, verified: read the paper →

Ground Truth. (2026, August 1). The non-sofic group is the one OpenAI claim a computer can check. Ground Truth. https://groundtruth.day/news/the-non-sofic-group-is-the-openai-claim-a-computer-can-check.html

@misc{groundtruth:the-non-sofic-group-is-the-openai-claim-a-computer-can-check,
  title  = {The non-sofic group is the one OpenAI claim a computer can check},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {aug},
  url    = {https://groundtruth.day/news/the-non-sofic-group-is-the-openai-claim-a-computer-can-check.html}
}

Topics: openai · mathematics · formal-verification · lean · group-theory · research