⚛️ quantum physics

An Explicit Counterexample to Tsirelson's Problem via a Linear System Game

This paper presents an explicit binary linear system game with over 1.4 million equations that serves as a concrete counterexample to Tsirelson's problem by demonstrating a perfect winning strategy in the commuting operator model while strictly limiting the success probability of all finite-dimensional quantum strategies.

Original authors: Minbo Gao, Tianshi Yu, Lihong Zhi

Published 2026-10-08

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Minbo Gao, Tianshi Yu, Lihong Zhi

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

In the strange and counterintuitive world of quantum physics, particles can become linked in ways that defy our everyday experience. When two such particles are measured, the result of one can instantly influence the result of the other, no matter how far apart they are. Scientists have long used these "entangled" particles to play a specific kind of game with two players who cannot talk to each other. The goal is to coordinate their answers to a referee's questions in a way that seems impossible if they were just using ordinary, classical logic. For decades, a fundamental question hung over this field: if the players are allowed to use the most powerful, infinite-dimensional quantum resources available, can they always achieve a perfect score? Or is there a subtle limit that even the most advanced quantum mechanics cannot cross? This question, known as Tsirelson's problem, was not just a technical puzzle; it was a gateway to understanding the very structure of reality and whether the mathematical models we use to describe the universe are complete.

A team of researchers has now settled this question with a definitive "no." They have constructed a specific, concrete game that proves a gap exists between what is possible with finite quantum systems and what is possible with infinite ones. In this game, the players can achieve a perfect score if they are allowed to use an infinite, theoretical resource known as a commuting operator strategy. However, if the players are restricted to any finite amount of quantum space, no matter how large, they will always fail to reach that perfect score. The researchers did not just suggest this gap might exist; they built the exact blueprint for the game, calculated its limits with absolute precision, and verified every step of their logic using a computer proof system.

The game itself is a variation of a logic puzzle involving a grid of equations. Imagine a massive sheet of paper filled with thousands of rows. Each row contains three specific variables that must add up to a certain number, either zero or one, following the rules of binary arithmetic. The players are given a single row and a single variable from that row. One player must provide a set of three numbers that satisfy the row's equation, while the other player must provide the value of the specific variable they were asked about. To win, their answers must be consistent with each other and satisfy the hidden rules of the grid. The researchers designed a grid so complex that it contains over 1.4 million rows and nearly 1.9 million variables. Every single row in this massive system has exactly three non-zero entries, creating a tightly woven web of constraints.

The brilliance of the construction lies in how it traps the players. The researchers proved that if the players try to win using any finite quantum system, they are mathematically forced to make a mistake. No matter how they tune their quantum devices, there is a hard ceiling on their success rate. They calculated that the best possible score for a finite quantum strategy is strictly less than one hundred percent. In fact, the gap between the perfect score and the best finite score is tiny but measurable, bounded by a fraction that is roughly one in 4.25 million. This means that even if the players had access to a quantum computer with more memory than there are atoms in the universe, they still could not win every single time.

However, the story changes completely when the players are allowed to use the infinite resource. The researchers showed that if the players utilize a strategy based on commuting operators—a mathematical framework that allows for infinite dimensions—they can achieve a perfect score every single time. They constructed a specific strategy that wins with one hundred percent certainty. This creates a clear separation: the set of correlations achievable with finite quantum systems is fundamentally different from the set achievable with infinite ones. The game acts as a litmus test, proving that the infinite world of quantum mechanics contains possibilities that can never be approximated by any finite collection of parts.

To ensure this result was beyond doubt, the team did not rely on hand-waving arguments or rough estimates. They translated the entire construction, including the massive grid of equations and the complex logic of the winning strategies, into a formal language that a computer can read and verify. Using a proof assistant called Lean, they checked every logical step, from the definition of the game to the calculation of the exact winning probabilities. The computer confirmed that the game has exactly 1,417,152 equations and 1,889,684 variables, and that the classical limit—the best score achievable with no quantum help at all—is exactly one minus one over 4,251,456. This level of rigor means the result is not just a strong mathematical argument, but a formally verified fact.

The implications of this discovery reach far beyond the specific game they built. It resolves a decades-old debate about the nature of quantum correlations. For years, physicists wondered if the strange behaviors of infinite quantum systems were just a theoretical curiosity that could be mimicked by large enough finite systems. This paper proves that they cannot. There are quantum phenomena that are inherently infinite and cannot be captured by any finite approximation. The researchers have provided a concrete example, a specific set of rules that separates the finite from the infinite, showing that the universe of quantum mechanics is richer and more complex than previously thought. By building this explicit counterexample, they have drawn a sharp line in the sand, demonstrating that some doors in the quantum world can only be opened with infinite keys.

Technical Summary: An Explicit Counterexample to Tsirelson's Problem via a Linear System Game

Problem Statement
The paper addresses Tsirelson's approximation problem, which asks whether the set of quantum correlations achievable by measurements on finite-dimensional tensor product Hilbert spaces ( $C_{qa}$ ) is equal to the set of correlations achievable by commuting measurements on a single Hilbert space of arbitrary dimension ( $C_{qc}$ ). This question is equivalent to Connes' embedding conjecture. While Ji, Natarajan, Vidick, Wright, and Yuen [JNV+20] previously provided a negative answer using recursive compression of nonlocal games, their construction was not explicit in the sense that the defining data could not be fully generated and stored. This paper aims to construct an explicit binary linear system game that separates $C_{qa}$ from $C_{qc}$ , providing a concrete counterexample where a perfect commuting operator strategy exists, but no sequence of finite-dimensional quantum strategies can achieve a success probability of 1.

Methodology
The authors construct a specific binary linear system game $G(A, b)$ derived from a finitely presented group $\Sigma = \Gamma(A, b)$ , known as the solution group. The methodology proceeds through several rigorous stages:

Group-Theoretic Construction:
- The construction begins with a pair of finitely presented groups $(Q, H)$ where both possess Kazhdan's property (T). $H$ is an "infranormal" subgroup of $Q$ , and there exists an element $t \in Q$ such that $tHt^{-1} \subsetneq H$ (strict compression).
- Using an amalgamated double $D = Q *_H Q$ , the authors construct an element $w$ of infinite order that is "uniformly asymptotically trivial." This means that for any homomorphism from $D$ into the unitary group of a tracial matrix ultraproduct, $w$ must map to the identity, despite being non-trivial in the group.
- An HNN extension is then applied to $D$ to introduce a central involution $J$ and a stable letter $z$ satisfying $zwz^{-1} = wJ$ . This forces $J$ to be non-trivial in the group $\Lambda$ but to map to the identity in any tracial matrix ultraproduct representation.
Embedding into a Linear System:
- The group $\Lambda$ is embedded into the solution group $\Sigma$ of a binary linear system $A\xi = b$ over $\mathbb{F}_2$ . This utilizes Slofstra's "wagon wheel" construction and involution substitution theorems [Slo20].
- The embedding preserves the non-triviality of the central involution $J$ , mapping it to the distinguished central involution $J_\Sigma$ of the solution group.
- The system is explicitly defined with specific dimensions: $m = 1,417,152$ equations and $n = 1,889,684$ variables. Every equation has exactly three non-zero coefficients, and the right-hand side vector $b$ has a single non-zero entry.
Formalization:
- The entire construction, including the group presentations, the linear system, and the proofs of the separation, is formalized in Lean 4 using the Mathlib library. This ensures the correctness of the combinatorial data and the logical steps without reliance on unverified hypotheses.

Key Contributions and Results

Explicit Counterexample: The paper presents a finite nonlocal game $G$ with two players and binary answers such that:
$\omega_q(G) = \omega_{qa}(G) < 1 = \omega_{qc}(G)$
Here, $\omega_{qc}(G) = 1$ is achieved by a perfect commuting operator strategy, while $\omega_{qa}(G)$ is strictly less than 1, meaning no finite-dimensional quantum strategy (or limit thereof) can win with probability 1.
Exact Classical Value: The authors compute the exact classical value of the game:
$\omega_c(G) = 1 - \frac{1}{4,251,456}$
This value is derived from the fact that the linear system $A\xi = b$ has no solution over $\mathbb{F}_2$ due to a parity obstruction (the sum of rows implies $0=1$ ), but a deterministic strategy can lose exactly one incidence.
Quantitative Gap: The paper establishes explicit bounds on the gap between the commuting and quantum values:
$2^{-250003} \leq 1 - \omega_q(G) \leq \frac{1}{4,251,456}$
The lower bound is independent of local dimensions, proving that the gap does not vanish as dimensions grow.
Uniform Asymptotic Triviality: A central technical result is the proof that the distinguished central involution $J_\Sigma$ is non-trivial in the group $\Sigma$ , yet for every $\eta > 0$ , there exists a $\delta > 0$ such that any homomorphism $f: F(S_\Sigma) \to U(d)$ with relation errors less than $\delta$ must satisfy $\|f(J_\Sigma) - I_d\|_{2,d} < \eta$ . This uniform asymptotic triviality prevents the existence of a sequence of finite-dimensional representations converging to a perfect strategy.

Significance
The paper claims significance by providing the first explicit counterexample to Tsirelson's problem in its approximation form, where the defining data (the matrix $A$ and vector $b$ ) can be generated, stored, and verified. Unlike previous existential proofs, this construction allows for the exact calculation of the classical value and the formal verification of the separation in a proof assistant (Lean 4). The work bridges the gap between abstract group theory (Kazhdan groups, property (T)) and quantum information theory, demonstrating that the failure of the approximation property is not merely a theoretical possibility but a concrete feature of specific nonlocal games. The formalization ensures that the massive combinatorial data required for the game (over 1.4 million equations) is free of error, solidifying the result as a definitive refutation of the conjecture $C_{qa} = C_{qc}$ .

Technical Summary: An Explicit Counterexample to Tsirelson's Problem via a Linear System Game

More like this