Papers With

← All papers
First page of An Explicit Counterexample to Tsirelson's Problem via a Linear System Game

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

Minbo Gao, Tianshi Yu, Lihong Zhi

quant-ph Oct 7, 2026 · v1 math.FA math.OA
formalization mathlib quantum algebra
Read PDF arXiv abstract Code
TL;DR
The explicit binary linear system is specified in Lean 4, and the C_qa/C_qc separation, exact classical value and quantum-gap bounds are formalized using Mathlib.
Abstract
We construct an explicit binary linear system game that separates \(C_{qa}\), the closure of the set of finite dimensional quantum correlations, from \(C_{qc}\), the set of commuting operator correlations. The game admits a perfect commuting operator strategy, while every correlation in \(C_{qa}\) has a success probability strictly less than 1. This provides a concrete counterexample to Tsirelson's problem in its approximation form. The defining system has \(1{,}417{,}152\) equations in \(1{,}889{,}684\) variables, with exactly three nonzero coefficients per equation and a single nonzero entry on the right hand side. We also compute the classical value exactly. The complete system is specified in Lean 4, and the separation and exact classical value are formalized using Mathlib.
Problem

Tsirelson's problem asks whether the closure C_qa of finite-dimensional quantum correlations equals the commuting-operator correlations C_qc. Ji et al. gave a negative answer non-constructively through recursive compression, and no explicit separating game was known.

Approach

A finitely presented Kazhdan group pair with strict compression is built from Ershov–Jaikin-Zapirain Kazhdan covers. An amalgamated double and an HNN extension then yield a nontrivial central involution that becomes trivial in every tracial matrix ultraproduct, following Thom's normalization theorem and the Alekseev–Liu–Thom spectral gap. Slofstra's embedding and wagon-wheel constructions turn this group into an explicit binary linear system game. The full system and the main results are formalized in Lean 4 with Mathlib, and a public repository fixes versions and includes axiom audits.

Results

The game has 1,417,152 equations in 1,889,684 variables. It admits a perfect commuting-operator strategy, while ω_q = ω_qa < 1. Lean proves the exact classical value 1 − 1/4,251,456 and the bounds 2^{-2^{50003}} ≤ 1 − ω_q ≤ 1/4,251,456.