Formalize Open Quantum Problem #33: Bell inequalities and operator algebras

### What is the conjecture

This is problem [#33](https://oqp.iqoqi.oeaw.ac.at/bell-inequalities-and-operator-algebras) in the later [Open Quantum Problems collection](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems), a community-maintained continuation of [Reinhard F. Werner's original collection](https://arxiv.org/abs/quant-ph/0504166).

**Status:** this problem is listed as **solved** on the [Solved Quantum Problems](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems) page (solved by Ji–Natarajan–Vidick–Wright–Yuen, 2020; see below).

> **Problem (Open Quantum Problem #33: “Bell inequalities and operator algebras”).**
> Quantum Bell-type inequalities are defined in terms of two (or more) subsystems of a quantum system. The subsystems may be treated either via local Hilbert spaces — tensor factors of a global Hilbert space — or via commuting local operator algebras on a single Hilbert space. The latter approach is less restrictive: it only requires that observables belonging to different subsystems commute.
>
> Are these two approaches equivalent?

Concretely, fix finite question sets `X,Y` and answer sets `A,B`, and consider bipartite correlations `p(a,b|x,y)`.

A correlation is in the **tensor-product model** if there exist Hilbert spaces `H_A`, `H_B`, a unit vector `ψ ∈ H_A ⊗ H_B`, and POVMs `{E_x^a}_a ⊂ B(H_A)`, `{F_y^b}_b ⊂ B(H_B)` such that
`p(a,b|x,y) = ⟨ψ, (E_x^a ⊗ F_y^b) ψ⟩`.

A correlation is in the **commuting-operator model** if there exist a Hilbert space `H`, a unit vector `ψ ∈ H`, and POVMs `{E_x^a}_a, {F_y^b}_b ⊂ B(H)` with
`[E_x^a, F_y^b] = 0` for all `x,y,a,b`, such that
`p(a,b|x,y) = ⟨ψ, E_x^a F_y^b ψ⟩`.

The original question asks whether every commuting-operator correlation is already realizable in the tensor-product model. A weaker / approximation version asks whether every commuting-operator correlation can at least be approximated arbitrarily well by **finite-dimensional** tensor-product correlations (closure taken in the usual finite-dimensional topology on the table of probabilities `p(a,b|x,y)`).

**Solved statement to formalize (Ji–Natarajan–Vidick–Wright–Yuen, 2020):**
The approximation question has a **negative** answer. There exist finite question/answer alphabets `X,Y,A,B` and a commuting-operator correlation `p(a,b|x,y)` that does **not** lie in the closure of the finite-dimensional tensor-product correlations for that scenario. In the standard notation for quantum correlation sets, for some finite Bell scenario one has
`C_qa(X,Y,A,B) ⊊ C_qc(X,Y,A,B)`.

Equivalently, there exists a finite two-player nonlocal game (or Bell functional) whose optimal value in the commuting-operator model is **strictly larger** than the supremum achievable by finite-dimensional tensor-product strategies, even after taking limits of such strategies.

This settles the density question from the OQP page in the negative: the tensor-product model is not dense in the commuting-operator model.

**Important structure / caveats:**
- In the finite-dimensional bipartite setting, the tensor-product and commuting-operator pictures are equivalent.
- Slofstra (2016/2020) already showed exact nonequivalence: there are nonlocal games with perfect commuting-operator strategies but no perfect tensor-product strategies.
- Ji et al. resolve the stronger approximation / closure question, and via earlier work of Junge–Navascués–Palazuelos–Pérez-García–Scholz–Werner and Fritz this also gives a negative resolution of Connes’ embedding problem / Kirchberg’s QWEP conjecture.

### Where to find the details / references

Primary sources:
- [Open Quantum Problems site (Problem #33)](https://oqp.iqoqi.oeaw.ac.at/bell-inequalities-and-operator-algebras)
- [Solved Quantum Problems list (shows #33 solved)](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems)
- [Werner / Krüger–Werner arXiv snapshot of the earlier collection](https://arxiv.org/abs/quant-ph/0504166) (historical background; the 2005 snapshot lists problems 1–29, while #33 appears on the later website)

Key solution reference (as cited on the OQP page):
- Z. Ji, A. Natarajan, T. Vidick, J. Wright, and H. Yuen, **“MIP*=RE”**, arXiv: [2001.04383](https://arxiv.org/abs/2001.04383); see also *Communications of the ACM* 64(11), 131–138 (2021)

Related / partial results mentioned on the OQP page (useful background for a formalization roadmap):
- B. S. Tsirelson, **“Some results and problems on quantum Bell-type inequalities”**, *Hadronic Journal Supplement* 8, 329–345 (1993)
- V. B. Scholz and R. F. Werner, **“Tsirelson’s Problem”**, arXiv: [0812.4305](https://arxiv.org/abs/0812.4305)
- M. Junge, M. Navascués, C. Palazuelos, D. Pérez-García, V. B. Scholz, and R. F. Werner, **“Connes’ embedding problem and Tsirelson’s problem”**, *J. Math. Phys.* 52, 012102 (2011); arXiv: [1008.1142](https://arxiv.org/abs/1008.1142)
- T. Fritz, **“Tsirelson’s problem and Kirchberg’s conjecture”**, *Rev. Math. Phys.* 24(5), 1250012 (2012); arXiv: [1008.1168](https://arxiv.org/abs/1008.1168)
- N. Ozawa, **“About the Connes embedding conjecture: algebraic approaches”**, *Jpn. J. Math.* 8(1), 147–183 (2013)
- W. Slofstra, **“Tsirelson’s problem and an embedding theorem for groups arising from non-local games”**, *J. Amer. Math. Soc.* 33, 1–56 (2020); arXiv: [1606.03140](https://arxiv.org/abs/1606.03140)
- M. Navascués, S. Pironio, and A. Acín, **“Bounding the set of quantum correlations”**, *Phys. Rev. Lett.* 98, 010401 (2007)

### Prerequisites needed

- Bell scenarios / nonlocal games: conditional probability tables `p(a,b|x,y)`, Bell inequalities, game values
- Basic quantum measurement formalism: Hilbert spaces, tensor products, unit vectors / states, POVMs, Born rule
- Operator-algebraic formulation of bipartite systems: commuting subalgebras, C\*-algebras or von Neumann algebras
- Basic convexity / topology of correlation sets: closure, density, separation by linear functionals
- (Background for the solution pathway) Tsirelson/Connes/Kirchberg equivalences and the NPA hierarchy / semidefinite relaxations

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

- ams-81 (Quantum theory)
- ams-46 (Functional analysis)
- ams-47 (Operator theory)

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [X] This issue is up for grabs: I would like to see this conjecture added by somebody else
---

Start with the solved statement for Open Quantum Problem #33 and the cited MIP*=RE paper, then inspect the repository's existing Lean formalizations for conventions and suitable entry points. Done means adding a checked formal statement of the negative approximation result, with the relevant definitions and supporting lemmas formalized as needed.

Written by the indexing model from the issue text.