For years, Tsirelson’s problem was one of the cleanest open questions linking quantum information to operator algebras: can every correlation produced by commuting measurements on a single Hilbert space be approximated by measurements on finite-dimensional tensor products? The 2020 MIP*=RE result of Ji, Natarajan, Vidick, Wright and Yuen answered “no”. A new preprint by Minbo Gao, Tianshi Yu and Lihong Zhi does something different: it writes down a specific, finite nonlocal game that witnesses the separation, computes its classical value exactly, and checks the main claims in the Lean 4 proof assistant.
This article was drafted with Claude and fact-checked against the cited primary sources.
Why this paper is worth reading
Knowing that a separating game exists is different from holding one. The authors construct a binary linear system game with 1,417,152 equations in 1,889,684 variables, each equation involving exactly three variables, and a right-hand side with a single nonzero entry. They prove that commuting-operator players can win it with probability 1, while every strategy in Cqa (the closure of finite-dimensional quantum correlations) succeeds with probability strictly less than 1. The complete system is specified in Lean 4, and the separation and the exact classical value are formalized using Mathlib.
What the paper does
The paper works with the standard correlation sets for a two-player game: Cq (finite-dimensional tensor-product strategies), its closure Cqa, and Cqc (commuting-operator strategies on one Hilbert space of arbitrary dimension). Tsirelson’s problem in its approximation form asks whether Cqa = Cqc; the paper notes that this is equivalent to Connes’ embedding conjecture.
The main results, as stated by the authors:
A finite two-player game G with payoffs in {0,1} satisfying ωq(G) = ωqa(G) < 1 = ωqc(G), so Cqa ≠ Cqc for its question and answer sets.
The exact classical value: ωc(G) = 1 − 1/4,251,456 (the game has 3m = 4,251,456 equally likely question pairs).
Explicit bounds on the quantum gap: 2^(−2^50003) ≤ 1 − ωq(G) ≤ 1/4,251,456, with the lower bound independent of the local dimension. This quantitative lower bound is proved in the Lean development (Remark 6.6).
The key idea
In a binary linear system game, Alice receives an equation and returns values for its three variables; Bob receives one variable and returns its value. They win if Alice’s values satisfy the parity constraint and agree with Bob’s. Earlier work by Cleve, Liu and Slofstra ties perfect commuting strategies to an algebraic object, the solution group of the system: a perfect commuting strategy exists exactly when a distinguished central involution J is nontrivial in that group. Slofstra and Vidick gave a matching criterion for the finite-dimensional side: the quantum value equals 1 only if there are approximate matrix representations of the solution group, with relation errors tending to zero, in which J stays a fixed distance from the identity.
So the task reduces to group theory: build a finitely presented solution group in which J is genuinely nontrivial, yet is forced towards the identity in every approximate unitary matrix representation, uniformly in the matrix dimension. The authors call this property uniform asymptotic triviality.
How the construction works
The paper assembles the group in stages, each with explicit generators and relations:
A Kazhdan pair. A finitely presented group Q on 48 generators and a subgroup H generated by 24 specified elements, both with Kazhdan’s property (T), built from finitely presented Kazhdan covers of Ershov and Jaikin-Zapirain over the field with five elements. A shear element t compresses H strictly into itself (tHt−1 is a proper subgroup of H); this is proved with a Laurent-polynomial matrix model.
Normalization. Thom’s normalization theorem, made unconditional by a spectral gap theorem of Alekseev, Liu and Thom, implies that in any homomorphism into a tracial matrix ultraproduct, a specified commutator word w in the amalgamated double Q *H Q is sent to the identity, even though w has infinite order in the group.
A central involution. An HNN-type extension adds a central involution J and a generator z with zwz−1 = wJ. J stays nontrivial in the group, but any representation that kills w must also kill J. The resulting group Λ has 74 generators.
Linearization. Slofstra’s embedding techniques (involution substitution and “wagon wheel” constructions) embed Λ into the solution group of an explicit binary linear system, with J mapped to the game’s distinguished involution. That system is the 1,417,152 × 1,889,684 matrix in the title result.
The perfect commuting strategy is then concrete: the left and right regular representations of the solution group, restricted to the subspace where J acts as −1. The classical value is also simple to pin down: because the system is inconsistent, every deterministic strategy loses at least one question pair, and the authors exhibit a strategy that loses exactly one.
Why it matters
MIP*=RE settled the yes/no question. This paper offers a finite object that can be generated, stored and checked. The authors state that the Lean results “use no admitted proofs or unproved mathematical hypotheses”, and the repository includes an axiom audit permitting only Lean’s standard axioms (propext, Classical.choice, Quot.sound). For a result whose informal proof chains together property (T), ultraproducts, combinatorial group theory and nonlocal games, a machine-checked end-to-end statement is a substantial form of evidence.
Technical perspective (interpretation)
The following is my reading, not a claim made by the authors. The quantitative bounds show how far this is from anything physically testable: the gap 1 − ωq is at least 2^(−2^50003) and at most about 2.4 × 10−7, and even the classical value is within 1/4,251,456 of perfect. The significance is mathematical and foundational: the separation becomes a certificate rather than an existence theorem. The paper also illustrates a route to Cqa ≠ Cqc through group-theoretic rigidity (Kazhdan groups and normalization) instead of the compression-of-games machinery behind MIP*=RE, and it sits alongside related work by Wang and Zhi that uses the same normalization mechanism for an explicit polynomial counterexample to Connes’ embedding conjecture. Whether the construction can be shrunk to something humanly inspectable is an open, interesting question.
Limitations and open questions
The gap is tiny and not effective in practice. The proven lower bound 2^(−2^50003) is astronomically small; the game is a mathematical witness, not an experimental proposal.
The formalization has a stated scope. Appendix B notes that some intermediate results are formalized only for the specific instance or only in the direction needed. For example, full injectivity of the map from Λ into the solution group is not formally proved (the authors explain why the weaker statements suffice), and only the needed implication of the Slofstra–Vidick criterion is formalized. The authors state that the correspondence between the formal definitions and the paper’s claims remains their responsibility.
Recent ingredients. Several cited inputs, including the Alekseev–Liu–Thom spectral gap theorem and Thom’s normalization theorem, are recent arXiv preprints. The Lean development formalizes the analytic ingredients it uses, according to the paper’s concordance tables, but expert review of the whole argument is still to come.
AI-assisted development. The paper’s AI-use declaration states that generative AI tools were used in mathematical exploration, the Lean code, and drafting; the authors state that they reviewed the proofs and the formalization and take full responsibility.
Size. With about 1.4 million equations, the game is explicit but large. Smaller separating games remain open.
Paper information
Title: An Explicit Counterexample to Tsirelson’s Problem via a Linear System Game
Authors: Minbo Gao (Institute of Software, CAS; UCAS; Tencent Hunyuan), Tianshi Yu (Institute of Software, CAS), Lihong Zhi (Academy of Mathematics and Systems Science, CAS; UCAS)
arXiv: 2610.10248v1, submitted 7 October 2026 (31 pages); quant-ph, cross-listed to math.FA and math.OA
Code: Lean 4 / Mathlib formalization on GitHub
Primary sources
Paper (abstract page): arxiv.org/abs/2610.10248
Full text (HTML): arxiv.org/html/2610.10248v1
Formalization repository: explicit-linear-system-game-formalization
Background: Ji, Natarajan, Vidick, Wright, Yuen, “MIP* = RE”, arXiv:2001.04383; Slofstra and Vidick, arXiv:1711.10676