An infinite symmetry system that finite shuffles cannot imitate
Can every infinite multiplication system be approximated by finite permutations?
Sofic groups encompass many major classes of groups, but whether every countable group is sofic remained open for decades.2Pestov This manuscript presents a concrete counterexample: the invertible elements of a binary Leavitt algebra contain a finitely generated group with no sufficiently accurate finite permutation models.1manuscript
A concrete starting point
Start with an infinite group of transformations. A finite model assigns selected group elements to permutations of a large finite set. It is accurate when the permutation assigned to a product agrees almost everywhere with composing the assigned permutations, while distinct elements remain distinguishable.2Pestov
A group is sofic if every finite set of its multiplication rules has arbitrarily accurate finite permutation models. The universal conjecture said that every countable group is sofic; the manuscript constructs one that is not.1manuscript2Pestov
The technical difficulty is that a finite model can decompose into many expander components, while elements of a commuting subgroup may transport points between those components. The new matching argument aligns transported components, selects one component with the required local behavior, and derives an impossible finite model of Thompson’s group V.8manuscript9manuscript
Each generator permutes the same finite set of points. Most short multiplication checks pass; the two red dashed links represent the permitted error set.
Why the earlier routes stopped short
The problem was not a shortage of exotic groups. It was proving that every sufficiently large finite permutation model must fail. Bowen and Burton showed that a non-sofic group would follow if a separate flexible-stability statement for certain higher-rank matrix groups held; that stability premise remained unproved.3Bowen
A later route through central extensions of p-adic lattices also reached non-soficity only under a permutation-stability hypothesis. These were genuine reductions, not counterexamples: the final bridge was still conditional.4Gohla
Kun supplied a powerful ingredient: after changing a vanishing fraction of edges, a sofic model of a property-(T) group breaks into expander graphs—networks where no small region is cheaply separated from the rest.5Kun Kun and Thom had also shown that if a commuting group acts beside a property-(T) group on one expander, then the commuting group must be LEF: every finite piece of its multiplication table embeds exactly into a finite group.6Kun
Kun gives many expander components. Kun–Thom needs one. A commuting permutation may exchange entire components, so selecting one component too early loses the subgroup action the argument must test.
The route attributed to Astra
OpenAI’s walkthrough describes a search through central extensions, one-sided inverses, mixing arguments, and a randomized logarithmic-binning idea before arriving at the final architecture. Its account singles out two moves: construct two compatible self-compressions inside a Leavitt algebra, then compare component sizes with a bounded median.7walkthrough
From a finite model to a contradiction
Why the Leavitt algebra matters
The binary Leavitt algebra has generators that make its underlying module behave like two copies of itself. A complete binary prefix code determines matrix coordinates, while restricting to a proper prefix determines a smaller corner with the same internal algebraic room. This is module self-similarity—not a claim that the ring and its matrix ring are identical as unital rings.9manuscript
Inside nine carefully chosen prefix cylinders, the construction places a property-(T) group Γ, a local copy J ≅ V on disjoint support, and two units u and v. The disjoint supports make Γ and J commute. Both compressors move Γ into the same smaller part of Γ; one also moves J into Γ; together Γ, u, and v generate the required ambient subgroup G.14manuscript
The component-matching move
Assume for contradiction that G has sofic models. Apply Kun’s theorem twice, once to Γ and once to G. For each ambient G-component A, assign a point x the size M(x) of its Γ-component, choose a weighted median mA, and use the bounded score f(x) = M(x)/(M(x)+mA). Because f stays between 0 and 1, small one-sided transport errors cannot accumulate without control.8manuscript
Expansion forces f close to 1/2 for almost every point. So a transported Γ-component and the Γ-component it mostly enters must have nearly equal size. Their overlap is eventually more than half the target, which makes the matching one-to-one: two disjoint transported components cannot each own a majority of the same target.15manuscript
The proof then chooses one matched component on which all required short-word tests pass, completes partial permutations, and removes another negligible bad region to restore uniform expansion. Kun–Thom now forces J to be LEF. But V is infinite, simple, and finitely presented; a finitely presented LEF group is residually finite, while an infinite simple group has no separating finite quotients. Contradiction.10Cannon16manuscript
Kun’s theorem produces many Γ-expander components, not one invariant component.
Expansion concentrates the bounded size score near ½. Majority overlap pairs transported components injectively.
Optional technical layer · the criterion in symbols
The general criterion begins with property-(T) groups Γ ≤ G, elements ti that satisfy tiΓti−1 ≤ Γ, and a finitely generated J with [Γ,J] = 1, Γ ∩ J = {1}, and t1Jt1−1 ≤ Γ. If Γ together with the ti generates G, the manuscript’s Proposition 2.3 says: G sofic ⇒ J LEF.17manuscript
For the explicit configuration, R = LF₂(1,2), G is the elementary group built from a nine-word prefix code, Γ is its three-word corner, t1 = u, t2 = v, and J is a local prefix copy of V. The proof verifies every hypothesis and obtains G not sofic; since subgroups of sofic groups are sofic, G ≤ R× implies R× is not sofic.18manuscript
What is proved—and what is not
Exact manuscript theorem: the unit group LF₂(1,2)× of the binary Leavitt algebra is not sofic. The manuscript proves this by constructing a finitely generated non-sofic subgroup G inside that unit group. It also extracts the existence of an infinite finitely presented non-sofic group from a finite failed approximation test.19manuscript
The released Lean file contains machine-checked declarations for the nine-prefix elementary group’s non-soficity and for the existence of a finitely presented non-sofic group. That is strong internal checking of the encoded statements, but it is not the same as an outside team independently formalizing the prose manuscript from scratch.11formal artifact
The result does not prove that this group is non-hyperlinear, does not settle its surjunctivity, and does not by itself invalidate every other finite-approximation framework. The manuscript explicitly leaves those questions open.12manuscript
Is the claim overhyped?
If independently validated, this is a major conjecture-level result: it supplies the counterexample needed to settle universal soficity negatively. The broader AI-development story remains less settled.
“A counterexample to the soficity conjecture.”
Yes, at the level of the released manuscript: one non-sofic countable group answers “are all countable groups sofic?” in the negative.20manuscript
“An explicit non-sofic group.”
Reasonable. The theorem names the concrete unit group LF₂(1,2)×, and the proof specifies a finitely generated subgroup through an explicit nine-prefix construction.21manuscript
“Astra solved it.”
This is OpenAI’s attribution. The announcement and walkthrough document that account, but neither is independent validation. Public expert review and reproduction remain the relevant next tests.13announcement
“AI has now solved group approximation.”
No. This resolves the universal soficity question, not hyperlinearity, surjunctivity, or the full landscape of approximation properties.22manuscript
Full bibliography
22 fully annotated sources
- 01 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — pp. 77–80; Theorem 1.1. The released manuscript and the source of the main theorem; not independent validation. ↩
- 02 · peer-reviewed predecessor
Vladimir Pestov. Hyperlinear and sofic groups: a brief guide — Bulletin of Symbolic Logic 14 (2008), Definition 3.1 and Open Question 3.8. A published pre-Astra survey of the definition and the then-open soficity conjecture. ↩
- 03 · peer-reviewed predecessor
Lewis Bowen and Peter Burton. Flexible stability and nonsoficity — Transactions of the AMS 373 (2020), Theorem 1.1. A conditional route through flexible permutation stability. ↩
- 04 · independent analysis
Lukas Gohla and Andreas Thom. High-dimensional expansion and soficity of groups — unpublished preprint, abstract and main theorem. Author preprint describing a conditional p-adic-lattice route; no journal reference is listed. ↩
- 05 · independent analysis
Gábor Kun. On sofic approximations of Property (T) groups — author preprint, Theorem 1. External predecessor providing the decomposition into a disjoint union of expanders; the cited record does not list a journal publication. ↩
- 06 · independent analysis
Gábor Kun and Andreas Thom. Inapproximability of actions and Kazhdan’s property (T) — author preprint, Theorem 1.1. External predecessor for the single-expander centralizer obstruction; the cited record does not list a journal publication. ↩
- 07 · reasoning walkthrough
OpenAI. Reasoning Walkthroughs: Constructing a Non-Sofic Group — Chapter 3, §§3.3–3.10, pp. 10–14. A retrospective discovery narrative; useful for route and dead ends, but not independent evidence. ↩
- 08 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — pp. 80–83, Proposition 2.3 and proof overview. States the expander-matching criterion and the bounded-median argument. ↩
- 09 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — pp. 89–92, Lemma 3.1, Proposition 3.2, proof of Theorem 1.1. The nine-cylinder Leavitt configuration and final contradiction. ↩
- 10 · authoritative reference
J. W. Cannon, W. J. Floyd, and W. R. Parry. Introductory notes on Richard Thompson’s groups — §6. Standard reference for Thompson’s group V, including finite presentation and simplicity. ↩
- 11 · formal certificate
OpenAI. NonSoficGroup.lean — lines 34600–34633. OpenAI-authored formalization artifact containing declarations for the local V-like group becoming LEF under the sofic assumption, the nine-prefix elementary group being non-sofic, and existence of a finitely presented non-sofic group; not an independent certification. ↩
- 12 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — pp. 78–79, “Related work”. Explicitly records unresolved consequences, including hyperlinearity and surjunctivity. ↩
- 13 · official announcement
OpenAI. Ten advances in mathematics — item 3. Evidence for OpenAI’s attribution and framing only; it is not independent mathematical review. ↩
- 14 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — pp. 89–92, Lemma 3.1 and Proposition 3.2. Verifies the commuting corners, two compressions, and ambient generation. ↩
- 15 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — pp. 82–89, proof of Proposition 2.3. Details median concentration, majority matching, component selection, and repair. ↩
- 16 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — pp. 92–93, proof of Theorem 1.1. The final LEF contradiction and subgroup implication. ↩
- 17 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — p. 83, Proposition 2.3. The abstract expander-matching criterion. ↩
- 18 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — pp. 89–93, §3 and proof of Theorem 1.1. Instantiation of the criterion in the binary Leavitt algebra. ↩
- 19 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — pp. 77–80 and p. 93. Main theorem and finitely presented consequence. ↩
- 20 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — Theorem 1.1. The theorem that supplies a negative answer to universal soficity. ↩
- 21 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — pp. 89–93. The explicit nine-prefix subgroup construction. ↩
- 22 · primary manuscript
OpenAI. A Counterexample to the Soficity Conjecture — pp. 78–79, “Related work”. Limits concerning hyperlinearity, surjunctivity, and adjacent conjectures. ↩