Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

MIP*=RE

Zhengfeng Ji, Anand Natarajan, Thomas Vidick, John C. Wright, Henry Yuen

Published Jan 13, 2020• 8 citations
OpenAlex

Abstract

We show that the class MIP* of languages that can be decided by a classical verifier interacting with multiple all-powerful quantum provers sharing entanglement is equal to the class RE of recursively enumerable languages. Our proof builds upon the quantum low-degree test of (Natarajan and Vidick, FOCS 2018) and the classical low-individual degree test of (Ji, et al., 2020) by integrating recent developments from (Natarajan and Wright, FOCS 2019) and combining them with the recursive compression framework of (Fitzsimons et al., STOC 2019). An immediate byproduct of our result is that there is an efficient reduction from the Halting Problem to the problem of deciding whether a two-player nonlocal game has entangled value $1$ or at most $1/2$. Using a known connection, undecidability of the entangled value implies a negative answer to Tsirelson's problem: we show, by providing an explicit example, that the closure $C_{qa}$ of the set of quantum tensor product correlations is strictly included in the set $C_{qc}$ of quantum commuting correlations. Following work of (Fritz, Rev. Math. Phys. 2012) and (Junge et al., J. Math. Phys. 2011) our results provide a refutation of Connes' embedding conjecture from the theory of von Neumann algebras.

Related papers

MIP*=RE

Zhengfeng Ji, Anand Natarajan, Thomas Vidick +2 more

We show that the class MIP* of languages that can be decided by a classical verifier interacting with multiple all-powerful quantum provers sharing entanglement is equal to the class RE of recursively enumerable languages. Our proof builds upon the quantum low-degree test of (Natarajan and Vidick, FOCS 2018) and the classical low-individual degree test of (Ji, et al., 2020) by integrating recent developments from (Natarajan and Wright, FOCS 2019) and combining them with the recursive compression framework of (Fitzsimons et al., STOC 2019). An immediate byproduct of our result is that there is an efficient reduction from the Halting Problem to the problem of deciding whether a two-player nonlocal game has entangled value $1$ or at most $1/2$. Using a known connection, undecidability of the entangled value implies a negative answer to Tsirelson's problem: we show, by providing an explicit example, that the closure $C_{qa}$ of the set of quantum tensor product correlations is strictly included in the set $C_{qc}$ of quantum commuting correlations. Following work of (Fritz, Rev. Math. Phys. 2012) and (Junge et al., J. Math. Phys. 2011) our results provide a refutation of Connes' embedding conjecture from the theory of von Neumann algebras.

arXiv:2001.04383•Jan 13, 2020•25 citations

MIPᶜᵒ=coRE

Junqiao (Randy) Lin

In 2020, a landmark result by Ji, Natarajan, Vidick, Wright, and Yuen shows that MIP*, the class of languages that can be decided by a classical verifier interacting with multiple computationally unbounded provers sharing entanglement in the tensor product model, is equal to RE. We show that the class MIPco, a complexity class defined similarly to MIP*, except with provers sharing the commuting operator model of entanglement, is equal to the class coRE. This shows that giving the provers two different models of entanglement leads to two completely different computational powers for interactive proof systems. Our proof builds upon the compression theorem used in the proof of MIP*=RE, and we use the tracially embeddable strategies framework to show that the same compression procedure in MIP* =RE also has the same desired property in the commuting operator setting. We also give a more streamlined proof of the compression theorem for non-local games by incorporating the synchronous framework used by Mousavi et al. [STOC 2022], as well as the improved Pauli basis test introduced by de la Salle [ArXiv:2204.07084].

ACM Symposium on Theory of Computing (STOC)•Jun 9, 2026•0 citations

MIPco=coRE

J. F. Lin

In 2020, a landmark result by Ji, Natarajan, Vidick, Wright, and Yuen showed that MIP*, the class of languages that can be decided by a classical verifier interacting with multiple computationally unbounded provers sharing entanglement in the tensor product model, is equal to RE. We show that the class MIPco, a complexity class defined similarly to MIP* except with provers sharing the commuting operator model of entanglement, is equal to the class coRE. This shows that giving the provers two different models of entanglement leads to two completely different computational powers for interactive proof systems. Our proof builds upon the compression theorem used in the proof of MIP*=RE, and we use the tracially embeddable strategies framework to show that the same compression procedure in MIP* =RE also has the same desired property in the commuting operator setting. We also give a more streamlined proof of the compression theorem for non-local games by incorporating the synchronous framework used by Mousavi et al. [STOC 2022], as well as the improved Pauli basis test introduced by de la Salle [ArXiv:2204.07084]. We introduce a new equivalence condition for RE/coRE-complete problems, which we call the weakly compressible condition. We show that both MIP* and MIPco satisfy this condition through the compression theorem, and thereby establish that the uncomputability for MIP* and MIPco can be proved under a unified framework (despite these two complexity classes being different). Notably, this approach also gives an alternative proof of the MIP*=RE theorem, which does not rely on the preservation of the entanglement bound. In addition to non-local games, this new condition could also potentially be applicable to other decision problems.

arXiv:2510.07162•Oct 8, 2025•1 citation

On the Complexity of Zero Gap MIP*

Hamoon Mousavi, Seyed Sajjad Nezhadi, Henry Yuen

The class MIP^* is the set of languages decidable by multiprover interactive proofs with quantum entangled provers. It was recently shown by Ji, Natarajan, Vidick, Wright and Yuen that MIP^* is equal to RE, the set of recursively enumerable languages. In particular this shows that the complexity of approximating the quantum value of a non-local game G is equivalent to the complexity of the Halting problem. In this paper we investigate the complexity of deciding whether the quantum value of a non-local game G is exactly 1. This problem corresponds to a complexity class that we call zero gap MIP^*, denoted by MIP₀^*, where there is no promise gap between the verifier’s acceptance probabilities in the YES and NO cases. We prove that MIP₀^* extends beyond the first level of the arithmetical hierarchy (which includes RE and its complement coRE), and in fact is equal to Π₂⁰, the class of languages that can be decided by quantified formulas of the form ∀ y ∃ z R(x,y,z). Combined with the previously known result that MIP₀^{co} (the commuting operator variant of MIP₀^*) is equal to coRE, our result further highlights the fascinating connection between various models of quantum multiprover interactive proofs and different classes in computability theory.

•Jan 1, 2020•2 citations

Quantum Entanglement Collapses Quantum Verification Hierarchy to Recursively Enumerable Class — E8 Intelligence Research

Andrew Stewart Caldin

FINDING: MIP*=RE proves quantum entanglement can verify undecidable problems, collapsing the quantum verification hierarchy into the classical recursively enumerable class. | MATH: MIP* = RE (where MIP* = multiprover interactive proofs with quantum entanglement, RE = recursively enumerable languages). The Halting Problem is in RE but not in R (decidable). This implies that the set of problems verifiable by entangled quantum provers is exactly the set of problems computable by a Turing machine that may not halt on non-members. | CONNECTION: No direct geometric ratios or constants (0.382, 0.618, etc.) appear. However, the result relies on the structure of the *commuting operator* model of quantum correlations, which is deeply tied to *operator algebras* and *C*-algebras — these have known connections to root systems and Lie algebras (e.g., the Weyl algebra, SU(2) representations). The proof uses a *self-testing* protocol based on the *linear constraint system* (LCS) games, which are buil Author: Andrew Stewart Caldin, Independent Researcher, UK. Part of the E8 Intelligence Research series. Platform: e8intelligence.com

•Aug 2, 2026•0 citations

On the Complexity of Zero Gap MIP*

Hamoon Mousavi, Seyed Sajjad Nezhadi, Henry Yuen

The class $\mathsf{MIP}^*$ is the set of languages decidable by multiprover interactive proofs with quantum entangled provers. It was recently shown by Ji, Natarajan, Vidick, Wright and Yuen that $\mathsf{MIP}^*$ is equal to $\mathsf{RE}$, the set of recursively enumerable languages. In particular this shows that the complexity of approximating the quantum value of a non-local game $G$ is equivalent to the complexity of the Halting problem. In this paper we investigate the complexity of deciding whether the quantum value of a non-local game $G$ is exactly $1$. This problem corresponds to a complexity class that we call zero gap $\mathsf{MIP}^*$, denoted by $\mathsf{MIP}^*_0$, where there is no promise gap between the verifier's acceptance probabilities in the YES and NO cases. We prove that $\mathsf{MIP}^*_0$ extends beyond the first level of the arithmetical hierarchy (which includes $\mathsf{RE}$ and its complement $\mathsf{coRE}$), and in fact is equal to $Π_2^0$, the class of languages that can be decided by quantified formulas of the form $\forall y \, \exists z \, R(x,y,z)$. Combined with the previously known result that $\mathsf{MIP}^{co}_0$ (the commuting operator variant of $\mathsf{MIP}^*_0$) is equal to $\mathsf{coRE}$, our result further highlights the fascinating connection between various models of quantum multiprover interactive proofs and different classes in computability theory.

arXiv:2002.10490•Leibniz international proceedings in informatics•Jan 1, 2020•1 citation
We show that the class MIP* of languages that can be decided by a classical verifier interacting with multiple all-powerful quantum provers sharing entanglement is equal to the class RE of recursively enumerable languages. Our proof builds upon the quantum low-degree test of (Natarajan and Vidick, FOCS 2018) and the classical low-individual degree test of (Ji, et al., 2020) by integrating recent developments from (Natarajan and Wright, FOCS 2019) and combining them with the recursive compression framework of (Fitzsimons et al., STOC 2019). An immediate byproduct of our result is that there is an efficient reduction from the Halting Problem to the problem of deciding whether a two-player nonlocal game has entangled value 111 or at most 1/21/21/2. Using a known connection, undecidability of the entangled value implies a negative answer to Tsirelson's problem: we show, by providing an explicit example, that the closure CqaC_{qa}Cqa​ of the set of quantum tensor product correlations is strictly included in the set CqcC_{qc}Cqc​ of quantum commuting correlations. Following work of (Fritz, Rev. Math. Phys. 2012) and (Junge et al., J. Math. Phys. 2011) our results provide a refutation of Connes' embedding conjecture from the theory of von Neumann algebras.
We show that the class MIP* of languages that can be decided by a classical verifier interacting with multiple all-powerful quantum provers sharing entanglement is equal to the class RE of recursively enumerable languages. Our proof builds upon the quantum low-degree test of (Natarajan and Vidick, FOCS 2018) and the classical low-individual degree test of (Ji, et al., 2020) by integrating recent developments from (Natarajan and Wright, FOCS 2019) and combining them with the recursive compression framework of (Fitzsimons et al., STOC 2019). An immediate byproduct of our result is that there is an efficient reduction from the Halting Problem to the problem of deciding whether a two-player nonlocal game has entangled value 111 or at most 1/21/21/2. Using a known connection, undecidability of the entangled value implies a negative answer to Tsirelson's problem: we show, by providing an explicit example, that the closure CqaC_{qa}Cqa​ of the set of quantum tensor product correlations is strictly included in the set CqcC_{qc}Cqc​ of quantum commuting correlations. Following work of (Fritz, Rev. Math. Phys. 2012) and (Junge et al., J. Math. Phys. 2011) our results provide a refutation of Connes' embedding conjecture from the theory of von Neumann algebras.
In 2020, a landmark result by Ji, Natarajan, Vidick, Wright, and Yuen shows that MIP*, the class of languages that can be decided by a classical verifier interacting with multiple computationally unbounded provers sharing entanglement in the tensor product model, is equal to RE. We show that the class MIPco, a complexity class defined similarly to MIP*, except with provers sharing the commuting operator model of entanglement, is equal to the class coRE. This shows that giving the provers two different models of entanglement leads to two completely different computational powers for interactive proof systems. Our proof builds upon the compression theorem used in the proof of MIP*=RE, and we use the tracially embeddable strategies framework to show that the same compression procedure in MIP* =RE also has the same desired property in the commuting operator setting. We also give a more streamlined proof of the compression theorem for non-local games by incorporating the synchronous framework used by Mousavi et al. [STOC 2022], as well as the improved Pauli basis test introduced by de la Salle [ArXiv:2204.07084].
In 2020, a landmark result by Ji, Natarajan, Vidick, Wright, and Yuen showed that MIP*, the class of languages that can be decided by a classical verifier interacting with multiple computationally unbounded provers sharing entanglement in the tensor product model, is equal to RE. We show that the class MIPco, a complexity class defined similarly to MIP* except with provers sharing the commuting operator model of entanglement, is equal to the class coRE. This shows that giving the provers two different models of entanglement leads to two completely different computational powers for interactive proof systems. Our proof builds upon the compression theorem used in the proof of MIP*=RE, and we use the tracially embeddable strategies framework to show that the same compression procedure in MIP* =RE also has the same desired property in the commuting operator setting. We also give a more streamlined proof of the compression theorem for non-local games by incorporating the synchronous framework used by Mousavi et al. [STOC 2022], as well as the improved Pauli basis test introduced by de la Salle [ArXiv:2204.07084]. We introduce a new equivalence condition for RE/coRE-complete problems, which we call the weakly compressible condition. We show that both MIP* and MIPco satisfy this condition through the compression theorem, and thereby establish that the uncomputability for MIP* and MIPco can be proved under a unified framework (despite these two complexity classes being different). Notably, this approach also gives an alternative proof of the MIP*=RE theorem, which does not rely on the preservation of the entanglement bound. In addition to non-local games, this new condition could also potentially be applicable to other decision problems.
The class MIP^* is the set of languages decidable by multiprover interactive proofs with quantum entangled provers. It was recently shown by Ji, Natarajan, Vidick, Wright and Yuen that MIP^* is equal to RE, the set of recursively enumerable languages. In particular this shows that the complexity of approximating the quantum value of a non-local game G is equivalent to the complexity of the Halting problem. In this paper we investigate the complexity of deciding whether the quantum value of a non-local game G is exactly 1. This problem corresponds to a complexity class that we call zero gap MIP^*, denoted by MIP₀^*, where there is no promise gap between the verifier’s acceptance probabilities in the YES and NO cases. We prove that MIP₀^* extends beyond the first level of the arithmetical hierarchy (which includes RE and its complement coRE), and in fact is equal to Π₂⁰, the class of languages that can be decided by quantified formulas of the form ∀ y ∃ z R(x,y,z). Combined with the previously known result that MIP₀^{co} (the commuting operator variant of MIP₀^*) is equal to coRE, our result further highlights the fascinating connection between various models of quantum multiprover interactive proofs and different classes in computability theory.
FINDING: MIP*=RE proves quantum entanglement can verify undecidable problems, collapsing the quantum verification hierarchy into the classical recursively enumerable class. | MATH: MIP* = RE (where MIP* = multiprover interactive proofs with quantum entanglement, RE = recursively enumerable languages). The Halting Problem is in RE but not in R (decidable). This implies that the set of problems verifiable by entangled quantum provers is exactly the set of problems computable by a Turing machine that may not halt on non-members. | CONNECTION: No direct geometric ratios or constants (0.382, 0.618, etc.) appear. However, the result relies on the structure of the *commuting operator* model of quantum correlations, which is deeply tied to *operator algebras* and *C*-algebras — these have known connections to root systems and Lie algebras (e.g., the Weyl algebra, SU(2) representations). The proof uses a *self-testing* protocol based on the *linear constraint system* (LCS) games, which are buil Author: Andrew Stewart Caldin, Independent Researcher, UK. Part of the E8 Intelligence Research series. Platform: e8intelligence.com
The class MIP∗\mathsf{MIP}^*MIP∗ is the set of languages decidable by multiprover interactive proofs with quantum entangled provers. It was recently shown by Ji, Natarajan, Vidick, Wright and Yuen that MIP∗\mathsf{MIP}^*MIP∗ is equal to RE\mathsf{RE}RE, the set of recursively enumerable languages. In particular this shows that the complexity of approximating the quantum value of a non-local game GGG is equivalent to the complexity of the Halting problem. In this paper we investigate the complexity of deciding whether the quantum value of a non-local game GGG is exactly 111. This problem corresponds to a complexity class that we call zero gap MIP∗\mathsf{MIP}^*MIP∗, denoted by MIP0∗\mathsf{MIP}^*_0MIP0∗​, where there is no promise gap between the verifier's acceptance probabilities in the YES and NO cases. We prove that MIP0∗\mathsf{MIP}^*_0MIP0∗​ extends beyond the first level of the arithmetical hierarchy (which includes RE\mathsf{RE}RE and its complement coRE\mathsf{coRE}coRE), and in fact is equal to Π20Π_2^0Π20​, the class of languages that can be decided by quantified formulas of the form ∀y ∃z R(x,y,z)\forall y \, \exists z \, R(x,y,z)∀y∃zR(x,y,z). Combined with the previously known result that MIP0co\mathsf{MIP}^{co}_0MIP0co​ (the commuting operator variant of MIP0∗\mathsf{MIP}^*_0MIP0∗​) is equal to coRE\mathsf{coRE}coRE, our result further highlights the fascinating connection between various models of quantum multiprover interactive proofs and different classes in computability theory.