8 Downstream results

Potential extensions of the project once the main theorem is in place. They are listed roughly in order of increasing formalization cost. The first two stay within finite-dimensional linear algebra plus elementary functional analysis, while the operator-algebraic consequences require von Neumann algebra infrastructure that largely does not yet exist in Mathlib and would constitute a major sub-project of independent value.

8.1 Uncomputability of the value

Corollary 7.2 is already a headline consequence requiring nothing further: no algorithm can approximate the (synchronous or quantum) value of a nonlocal game to within any constant better than \(\frac12\).

8.2 Separation of quantum and commuting values

Theorem 8.1 Separation

There is an explicit synchronous game \(\mathfrak {G}^{\textsc{Sep}}\) with \(\mathrm{val}^*(\mathfrak {G}^{\textsc{Sep}}) \leq \frac12\) and \(\mathrm{val}^{\mathrm{co}}(\mathfrak {G}^{\textsc{Sep}}) = 1\).

Sketch: apply the reduction of Theorem 6.9 to a machine that searches for a proof of its own non-halting (or any non-halting machine whose game retains a perfect commuting-operator strategy), and track through the pipeline that completeness holds not just for PCC strategies but for commuting-operator (equivalently, tracial) strategies. This commuting completeness property is an additional obligation on Sections 6.2–6.6 that the blueprint should make explicit when those sections are worked out; it is the only new ingredient beyond the main theorem. An alternative route: if \(\mathrm{val}^*= \mathrm{val}^{\mathrm{co}}\) for all games, then combining Lemma 3.13 (value approximable from below) with the NPA hierarchy [ 25 ] (commuting value approximable from above) would make the value computable, contradicting Corollary 7.2; this gives a non-explicit separation with much less work, and is the recommended first target.

8.3 Failure of Tsirelson’s problem

Corollary 8.2 Tsirelson’s problem, negative answer

There exist finite question and answer sets for which the closure \(C_{qa}\) of the set of finite-dimensional quantum correlations is strictly contained in the set \(C_{qc}\) of commuting-operator correlations.

Immediate from Theorem 8.1: the value gap is witnessed by a correlation in \(C_{qc}\) at distance bounded away from \(C_{qa}\). Requires only the definitions of the correlation sets. (Non-closure of the unclosed set \(C_q\) itself is Slofstra’s earlier theorem [ 13 ] , which also follows, with quantitative bounds, from the machinery here.)

8.4 Refutation of Connes’ Embedding Problem

Corollary 8.3 Connes’ Embedding Problem, negative answer

There is a separable II\(_1\) factor (indeed, a tracial von Neumann algebra generated by finitely many projections) that does not embed into an ultrapower \(\cal {R}^{\omega }\) of the hyperfinite II\(_1\) factor.

Source for the implication.

Tsirelson’s problem is equivalent to CEP by Fritz [ 15 ] and Junge et al. [ 14 ] , with the converse direction completed by Ozawa [ 16 ] . In the synchronous framework the implication is particularly direct: a synchronous correlation is precisely given by projections in a tracial von Neumann algebra summing to \(1\) [ 18 , 17 ] , and \(C_{qa}\)-type correlations are exactly those arising from \(\cal {R}^\omega \)-embeddable algebras, so Corollary 8.2 for synchronous correlations yields a non-embeddable algebra.

Comments.

This is the deepest formalization challenge on the list: it needs tracial von Neumann algebras, ultraproducts, and the synchronous-correlation correspondence. The synchronous framework adopted in this blueprint (Section 1.3) was chosen partly because it makes this bridge as short as it can be. A reasonable staging: (i) define \(C_{qa}, C_{qc}\) and synchronous correlations; (ii) prove the synchronous correlation–tracial algebra correspondence; (iii) formalize the ultraproduct \(\cal {R}^\omega \) and the equivalence. Step (iii) alone is a landmark for operator algebras in Lean.

8.5 Failure of Kirchberg’s QWEP conjecture

Corollary 8.4 QWEP

Kirchberg’s QWEP conjecture fails: there is a C\(^*\)-algebra that is not a quotient of a C\(^*\)-algebra with the weak expectation property; equivalently, \(C^*(F_2) \otimes _{\min } C^*(F_2) \neq C^*(F_2) \otimes _{\max } C^*(F_2)\).

Equivalent to CEP by Kirchberg’s theorem (see [ 16 ] ); no new input from the project, but the equivalence itself is another substantial operator-algebra formalization.

8.6 Further directions

Remark 8.5

Other candidate consequences to record as the project matures: undecidability of the existence of perfect strategies for synchronous games and its group-theoretic reformulations (via the synchronous algebra of a game); quantitative non-closure of \(C_q\) and rates for the NPA hierarchy; uncomputability results for entanglement requirements (\(\mathrm{Ent}(\cdot , \frac12)\) grows faster than any computable function along the halting games), which need the entanglement form of the pipeline (Remark 6.8) rather than the value form adopted here; the commuting-operator counterpart \(\mathrm{MIP}^{\mathrm{co}}= \mathrm{coRE}\) [ 9 , 10 ] , for which direct parallel repetition for commuting-operator strategies (Theorem 5.5) and Lin’s tracial density theorem (Theorem 5.8) are already formalized; and, more speculatively, connections to the undecidability of the spectral gap and to the existence of non-hyperlinear groups, the latter being not implied by CEP’s failure and best recorded as an open problem.

1: Z. Ji, A. Natarajan, T. Vidick, J. Wright, H. Yuen. \(\mathrm{MIP}^* = \mathrm{RE}\). arXiv:2001.04383, 2020 (revised 2022).
2: Z. Ji, A. Natarajan, T. Vidick, J. Wright, H. Yuen. Quantum soundness of the classical low individual degree test. arXiv:2009.12982, 2020.
3: A. Natarajan, J. Wright. \(\mathrm{NEEXP} \subseteq \mathrm{MIP}^*\). In Proc. 60th FOCS, 2019. arXiv:1904.05870.
4: W. T. Gowers, O. Hatami. Inverse and stability theorems for approximate representations of finite groups. Sbornik: Mathematics, 208(12):1784–1817, 2017. arXiv:1510.04085.
5: M. de la Salle. Orthogonalization of positive operator valued measures. arXiv:2103.14126, 2021.
6: T. Vidick. Almost synchronous quantum correlations. Journal of Mathematical Physics, 63(2):022201, 2022. arXiv:2103.02468.
7: M. Bavarian, T. Vidick, H. Yuen. Hardness amplification for entangled games via anchoring. In Proc. 49th STOC, 2017. arXiv:1509.07466.
8: A. Marks, S. S. Nezhadi, H. Yuen. The recursive compression method for proving undecidability results. Manuscript.
9: J. Lin. Tracially embeddable strategies: lifting MIP\(^*\) tricks to MIP\(^{\mathrm{co}}\). arXiv:2304.01940, 2023.
10: J. Lin. \(\mathrm{MIP}^{\mathrm{co}} = \mathrm{coRE}\). In Proc. 58th STOC, 2026. arXiv:2510.07162.
11: X. Wu, J.-D. Bancal, M. McKague, V. Scarani. Device-independent parallel self-testing of two singlets. Physical Review A, 93:062121, 2016. arXiv:1512.02074.
12: J. Fitzsimons, Z. Ji, T. Vidick, H. Yuen. Quantum proof systems for iterated exponential time, and beyond. In Proc. 51st STOC, 2019. arXiv:1805.12166.
13: W. Slofstra. The set of quantum correlations is not closed. Forum of Mathematics, Pi, 7:E1, 2019. arXiv:1703.08618.
14: M. Junge, M. Navascués, C. Palazuelos, D. Pérez-García, V. Scholz, R. Werner. Connes’ embedding problem and Tsirelson’s problem. Journal of Mathematical Physics, 52(1):012102, 2011.
15: T. Fritz. Tsirelson’s problem and Kirchberg’s conjecture. Reviews in Mathematical Physics, 24(05):1250012, 2012.
16: N. Ozawa. About the Connes embedding conjecture: algebraic approaches. Japanese Journal of Mathematics, 8(1):147–183, 2013.
17: S.-J. Kim, V. Paulsen, C. Schafhauser. A synchronous game for binary constraint systems. Journal of Mathematical Physics, 59(3):032201, 2018.
18: V. Paulsen, S. Severini, D. Stahlke, I. Todorov, A. Winter. Estimating quantum chromatic numbers. Journal of Functional Analysis, 270(6):2188–2222, 2016.
19: C. Papadimitriou, M. Yannakakis. A note on succinct representations of graphs. Information and Control, 71(3):181–185, 1986.
20: S. Cook. The complexity of theorem-proving procedures. In Proc. 3rd STOC, 1971.
21: V. Shoup. New algorithms for finding irreducible polynomials over finite fields. Mathematics of Computation, 54(189):435–447, 1990.
22: H. W. Lenstra, Jr. Finding isomorphisms between finite fields. Mathematics of Computation, 56(193):329–347, 1991.
23: J. Schwartz. Fast probabilistic algorithms for verification of polynomial identities. Journal of the ACM, 27(4):701–717, 1980.
24: R. Zippel. Probabilistic algorithms for sparse polynomials. In Symbolic and Algebraic Computation, pages 216–226, 1979.
25: M. Navascués, S. Pironio, A. Acín. A convergent hierarchy of semidefinite programs characterizing the set of quantum correlations. New Journal of Physics, 10(7):073013, 2008.
26: B. Durand, A. Romashchenko, A. Shen. Fixed-point tile sets and their applications. Journal of Computer and System Sciences, 78(3):731–764, 2012.
27: R. Raz. A parallel repetition theorem. SIAM Journal on Computing, 27(3):763–803, 1998.
28: T. Holenstein. Parallel repetition: simplification and the no-signaling case. Theory of Computing, 5(1):141–172, 2009.
29: R. Jain, S. Kundu. A direct product theorem for one-way quantum communication. In Proc. 36th CCC, 2021. arXiv:2008.08963.
30: OpenAI. Ten advances in mathematics and theoretical computer science. Chapter 6: Exponential parallel repetition for all two-player entangled games. 2026. https://cdn.openai.com/pdf/ten-proofs-oai.pdf; Lean formalization at https://github.com/openai/ten-proofs.
31: T. Vidick. Uniform direct parallel repetition for two-player commuting-operator strategies. Manuscript with Lean formalization, 2026. https://github.com/vidick/commuting-repetition.
32: A. Uhlmann. The “transition probability” in the state space of a \(*\)-algebra. Reports on Mathematical Physics, 9(2):273–279, 1976.
33: C. A. Fuchs, J. van de Graaf. Cryptographic distinguishability measures for quantum-mechanical states. IEEE Transactions on Information Theory, 45(4):1216–1227, 1999.
34: E. H. Lieb, M. B. Ruskai. Proof of the strong subadditivity of quantum-mechanical entropy. Journal of Mathematical Physics, 14(12):1938–1941, 1973.
35: M. M. Wilde. Quantum Information Theory. Cambridge University Press, 2013. arXiv:1106.1445.