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

arXiv:2609.12346

The Low-Individual-Degree Test Without the Diagonal-Lines Test Is Not Quantum-Sound

Honghao Fu, Nengkun Yu, Tianrun Zhao

quant-phcs.CCSubmitted Sep 11, 2026• Announced Sep 14, 2026• 0 citations• Revised Oct 19, 2026 (v2)
v1 · Sep 11, 2026v2 · Oct 19, 2026
arXivHTMLPDF

Abstract

To prove the quantum soundness of the classical low-individual-degree test, the authors of \cite{JNVWY20LID} defined three subtests, namely the axis-parallel lines test, the self-consistency test, and the diagonal-lines test. An interesting question is whether the diagonal-lines test can be removed. In this paper, we show that the diagonal-lines test cannot simply be removed without another compatibility mechanism. Consequently, replacing the "conditional linear functions" by "coordinate deletion functions" in the proof of MIP*=RE, as mentioned in \cite{JNVWY20LID}, does not by itself preserve the required soundness. The authors of \cite{JNVWY20LID} found an example that requires the diagonal-lines test when \((m, d, q) = (2, 2, 4)\); we give an example when \((m, d) = (2, 2)\) and \(q\) is any odd prime.

Related papers

Quantum Soundness of a Total-Degree Line-versus-Point Test

Honghao Fu, Nengkun Yu, Tianrun Zhao

We prove quantum soundness of the total-degree diagonal line-vs-point test using the individual-degree soundness theorem of Ji, Natarajan, Vidick, Wright, and Yuen. A random change of coordinates yields projective polynomial decoders of total degree at most $md$. The uniform-line slice of the test bounds the weight of outcomes of degree greater than $d$, which are removed by a common relabeling. This reduction does not yield a dimension-independent soundness bound: the $\operatorname{poly}(m)$ dependence of the individual-degree theorem persists, as discussed in Section 1.2 of arXiv:2009.12982.

quant-pharXiv:2609.27129•Sep 24, 2026•0 citations

Quantum soundness of testing tensor codes

Zhengfeng Ji, Anand Natarajan, Thomas Vidick +2 more

A locally testable code is an error-correcting code that admits very efficient probabilistic tests of membership. Tensor codes provide a simple family of combinatorial constructions of locally testable codes that generalize the family of Reed-Muller codes. The natural test for tensor codes, the axis-parallel line vs. point test, plays an essential role in constructions of probabilistically checkable proofs. We analyze the axis-parallel line vs. point test as a two-prover game and show that the test is sound against quantum provers sharing entanglement. Our result implies the quantum-soundness of the low individual degree test, which is an essential component of the MIP* = RE theorem. Our proof also generalizes to the infinite-dimensional commuting-operator model of quantum provers.

Annual Symposium on Foundations of Computer Science•Feb 1, 2022•7 citations

Quantum soundness of testing tensor codes

Zhengfeng Ji, Anand Natarajan, Thomas Vidick +2 more

A locally testable code is an error-correcting code that admits very efficient probabilistic tests of membership. Tensor codes provide a simple family of combinatorial constructions of locally testable codes that generalize the family of Reed-Muller codes. The natural test for tensor codes, the axis-parallel line vs. point test, plays an essential role in constructions of probabilistically checkable proofs. We analyze the axis-parallel line vs. point test as a two-prover game and show that the test is sound against quantum provers sharing entanglement. Our result implies the quantum-soundness of the low individual degree test, which is an essential component of the MIP* = RE theorem. Our proof also generalizes to the infinite-dimensional commuting-operator model of quantum provers.

arXiv:2111.08131•Nov 15, 2021•1 citation

Quantum soundness of the classical low individual degree test

Zhengfeng Ji, Anand Natarajan, Thomas Vidick +2 more

Low degree tests play an important role in classical complexity theory, serving as basic ingredients in foundational results such as $\mathsf{MIP} = \mathsf{NEXP}$ [BFL91] and the PCP theorem [AS98,ALM+98]. Over the last ten years, versions of these tests which are sound against quantum provers have found increasing applications to the study of nonlocal games and the complexity class~$\mathsf{MIP}^*$. The culmination of this line of work is the result $\mathsf{MIP}^* = \mathsf{RE}$ [arXiv:2001.04383]. One of the key ingredients in the first reported proof of $\mathsf{MIP}^* = \mathsf{RE}$ is a two-prover variant of the low degree test, initially shown to be sound against multiple quantum provers in [arXiv:1302.1242]. Unfortunately a mistake was recently discovered in the latter result, invalidating the main result of [arXiv:1302.1242] as well as its use in subsequent works, including [arXiv:2001.04383]. We analyze a variant of the low degree test called the low individual degree test. Our main result is that the two-player version of this test is sound against quantum provers. This soundness result is sufficient to re-derive several bounds on~$\mathsf{MIP}^*$ that relied on [arXiv:1302.1242], including $\mathsf{MIP}^* = \mathsf{RE}$.

arXiv:2009.12982•Sep 27, 2020•10 citations

Quantum soundness of testing tensor codes

Zhengfeng Ji, Anand Natarajan, Thomas Vidick +2 more

Quantum soundness of testing tensor codes, Discrete Analysis 2022:17, 73 pp. This paper proves an essential component of a major recent result in complexity theory, known as the MIP*=RE theorem, which was proved by the same authors. MIP* and RE are two important complexity classes with completely different definitions, and the fact that they are equal is a very deep and surprising fact, with implications not just for complexity theory but also for parts of pure mathematics, and in particular operator theory. RE is the class of recursively enumerable functions -- that is, Boolean functions $f$ for which there is an algorithm such that if $f(x)=1$, then the algorithm can establish this in finite time. Here there are no restrictions on how long the algorithm takes or how much memory it uses. The definition of MIP* is quite a lot less straightforward, but can be understood in a sequence of steps. First, the class P consists of Boolean functions that can be computed in polynomial time (in the length of the input). NP consists of Boolean functions $f:\{0,1\}^n\to\{0,1\}$ such that if $f(x)=1$ then this fact can be _verified_ in polynomial time. That is, for each $n$ there is some $m$ that depends polynomially on $n$ and a function $g:\{0,1\}^{n+m}\to\{0,1\}$ in $P$ such that for each $x$, $f(x)=1$ if and only if there exists $y\in\{0,1\}^m$ with $g(x,y)=1$. We can think of such a $y$ as a "certificate" that guarantees that $f(x)=1$. (For example, if $f$ detects whether there is a Hamilton cycle in a graph, $g$ could be the function that takes a graph and an ordering on the vertices and outputs 1 if and only if that ordering defines a Hamilton cycle.) We can think of NP in a slightly different way as a collaboration between two agents, a powerful prover and a much less powerful verifier. They can collaborate as follows. The verifier presents the prover with a string $x$. The prover, unconstrained by any time or space limitations, responds with a string $y$. The verifier then calculates $g(x,y)$. If $g(x,y)=1$ then $f(x)=1$ and otherwise $f(x)=0$. For this to work two properties of their protocol are needed. The first is _completeness_: that whenever $f(x)=1$ there is a suitable certificate $y$. The second is _soundness_: that whenever $f(x)=0$ there is no such certificate. We can imagine this as a situation where the prover always wants to convince the verifier that $f(x)=1$, regardless of whether that is actually true. If the protocol is both complete and sound, then in fact the verifier will always correctly determine the value of $f$. To obtain the class IP (which stands for "interactive proof") we modify the above situation slightly, allowing the verifier access to a string of random bits, allowing communication between the verifier and prover to take place over several rounds, and requiring at the end only that that verifier is _almost_ certain that $f(x)=1$. Rather than give a formal definition, we present here an example due to Goldreich, Micali and Wigderson of a protocol that shows that non-isomorphism of graphs is in IP (which is not obvious, since while it is easy to see that graph isomorphism belongs to NP, there is no particular reason to suppose that graph _non_-isomorphism does). The idea is simple: the verifier takes two graphs $G$ and $H$ and sends to the prover a sequence $(K_1,\dots,K_m)$ of graphs, where each $K_i$ is obtained by randomly picking one of $G$ and $H$ and randomly permuting its vertices. The prover then sends back a 01-sequence $x\in\{0,1\}^m$. Finally, the verifier judges $G$ and $H$ to be non-isomorphic if $x_i=1$ for all and only those $i$ for which $K_i$ is isomorphic to $G$ (which the verifier knows). If $G$ and $H$ are indeed non-isomorphic, the prover can ensure that the verifier will agree that this is the case, but otherwise the prover has no idea which $K_i$ came from which graph and can therefore do so with probability only $2^{-m}$. It turns out that IP is equal to the complexity class PSPACE, which consists of functions that can be computed with only a polynomial amount of memory (but with no restriction on time). This is already an indication of the power of interactive proofs. However, it turns out that with some simple modifications they can be made considerably more powerful. One modification is to have more than one prover and not to allow the provers to communicate. This makes it harder for the provers to fool the verifier if $f(x)\ne 1$, since the verifier can be on the lookout for inconsistencies in their answers. The resulting class MIP (for "multiprover interactive proof") turns out to be equivalent to the complexity class NEXPTIME, which is like NP except that the verification is now allowed to take an exponential amount of time, so it is a huge class. Finally, we come to MIP*. Here quantum entanglement comes into play. Before the computation starts the provers are allowed to share entangled quantum bits, which have the potential to create correlations between their responses to the verifier. Potentially at least, this greatly enlarges the set of possible strategies for the provers, and therefore greatly enlarges the class of functions that can be computed. And this potential turns out to be realized: the statement that MIP*=RE is telling us the extraordinary fact that every recursively enumerable function belongs to MIP*. That is, if you are given a Turing machine and asked whether it halts, there is some protocol involving multiple provers using entangled bits such that if the Turing machine halts, the provers will convince the verifer of that fact, and otherwise the verifier will be almost certain that it does not halt. Note that there is no algorithm that will establish (in general) that a Turing machine does _not_ halt, but the fact that MIP*=RE tells us that if we are satisfied with being _almost_ certain that it does not halt, then for each instance of the problem there is an MIP* protocol that will give that to us. This paper concerns a particular problem from coding theory. A _linear code_ is a subspace $\mathcal C$ of $\mathbb F^n$ for some finite field $\mathbb F$ such that any two elements, or _codewords_, differ in at least $d$ coordinates. (The bigger $d$ is, the better the code.) Given such a code, the tensor code $\mathcal C^{\otimes m}$ is defined to be the set of all functions $g:[n]^m\to\mathbb F$ (where $[n]$ denotes the set $\{1,2,\dots,n\}$) such that if you fix all but one coordinate, then the resulting restriction of $g$, regarded as an element of $\mathbb F^n$ in the obvious way, is an element of $\mathbb C$. The corresponding computational problem is to determine whether a given function $g$ belongs to $\mathcal C^{\otimes m}$. Such codes are called _locally testable_ because there is a simple protocol that allows an interactive proof based on only local information. It works as follows. The verifier chooses a random element $x$ of $[n]^m$, the prover responds with an element $u\in\mathbb F$, the verifier then chooses a random $j\in[n]$, and the prover responds with a codeword $w$ from $\mathcal C$. If $w_j=u$, then the verifier judges $g$ to belong to $\mathcal C^{\otimes m}$. Note that if $g$ does indeed belong to $\mathcal C^{\otimes m}$, then all the prover has to do is choose the word obtained from the line of all points $y$ such that $y_i=x_i$ when $i\ne j$. Soundness of the protocol is less obvious (and requires a further technical condition on the code called interpolability) but follows quickly from a result of Babai, Fortnow and Lund. The main result of this paper can be thought of as saying that two interative provers cannot do significantly better for this problem if they are allowed to use entangled bits than if they are restricted to classical computation. For more details about tensor codes, this result, and how it relates to the MIP*=RE theorem, the extensive introduction to the paper itself is highly recommended.

•Dec 1, 2022•0 citations

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.

•Jan 13, 2020•8 citations
To prove the quantum soundness of the classical low-individual-degree test, the authors of \cite{JNVWY20LID} defined three subtests, namely the axis-parallel lines test, the self-consistency test, and the diagonal-lines test. An interesting question is whether the diagonal-lines test can be removed. In this paper, we show that the diagonal-lines test cannot simply be removed without another compatibility mechanism. Consequently, replacing the "conditional linear functions" by "coordinate deletion functions" in the proof of MIP*=RE, as mentioned in \cite{JNVWY20LID}, does not by itself preserve the required soundness.
The authors of \cite{JNVWY20LID} found an example that requires the diagonal-lines test when ((m, d, q) = (2, 2, 4)); we give an example when ((m, d) = (2, 2)) and (q) is any odd prime.
We prove quantum soundness of the total-degree diagonal line-vs-point test using the individual-degree soundness theorem of Ji, Natarajan, Vidick, Wright, and Yuen. A random change of coordinates yields projective polynomial decoders of total degree at most mdmdmd. The uniform-line slice of the test bounds the weight of outcomes of degree greater than ddd, which are removed by a common relabeling. This reduction does not yield a dimension-independent soundness bound: the poly⁡(m)\operatorname{poly}(m)poly(m) dependence of the individual-degree theorem persists, as discussed in Section 1.2 of arXiv:2009.12982.
A locally testable code is an error-correcting code that admits very efficient probabilistic tests of membership. Tensor codes provide a simple family of combinatorial constructions of locally testable codes that generalize the family of Reed-Muller codes. The natural test for tensor codes, the axis-parallel line vs. point test, plays an essential role in constructions of probabilistically checkable proofs. We analyze the axis-parallel line vs. point test as a two-prover game and show that the test is sound against quantum provers sharing entanglement. Our result implies the quantum-soundness of the low individual degree test, which is an essential component of the MIP* = RE theorem. Our proof also generalizes to the infinite-dimensional commuting-operator model of quantum provers.
A locally testable code is an error-correcting code that admits very efficient probabilistic tests of membership. Tensor codes provide a simple family of combinatorial constructions of locally testable codes that generalize the family of Reed-Muller codes. The natural test for tensor codes, the axis-parallel line vs. point test, plays an essential role in constructions of probabilistically checkable proofs. We analyze the axis-parallel line vs. point test as a two-prover game and show that the test is sound against quantum provers sharing entanglement. Our result implies the quantum-soundness of the low individual degree test, which is an essential component of the MIP* = RE theorem. Our proof also generalizes to the infinite-dimensional commuting-operator model of quantum provers.
Low degree tests play an important role in classical complexity theory, serving as basic ingredients in foundational results such as MIP=NEXP\mathsf{MIP} = \mathsf{NEXP}MIP=NEXP [BFL91] and the PCP theorem [AS98,ALM+98]. Over the last ten years, versions of these tests which are sound against quantum provers have found increasing applications to the study of nonlocal games and the complexity class~MIP∗\mathsf{MIP}^*MIP∗. The culmination of this line of work is the result MIP∗=RE\mathsf{MIP}^* = \mathsf{RE}MIP∗=RE [arXiv:2001.04383]. One of the key ingredients in the first reported proof of MIP∗=RE\mathsf{MIP}^* = \mathsf{RE}MIP∗=RE is a two-prover variant of the low degree test, initially shown to be sound against multiple quantum provers in [arXiv:1302.1242]. Unfortunately a mistake was recently discovered in the latter result, invalidating the main result of [arXiv:1302.1242] as well as its use in subsequent works, including [arXiv:2001.04383]. We analyze a variant of the low degree test called the low individual degree test. Our main result is that the two-player version of this test is sound against quantum provers. This soundness result is sufficient to re-derive several bounds on~MIP∗\mathsf{MIP}^*MIP∗ that relied on [arXiv:1302.1242], including MIP∗=RE\mathsf{MIP}^* = \mathsf{RE}MIP∗=RE.
Quantum soundness of testing tensor codes, Discrete Analysis 2022:17, 73 pp. This paper proves an essential component of a major recent result in complexity theory, known as the MIP*=RE theorem, which was proved by the same authors. MIP* and RE are two important complexity classes with completely different definitions, and the fact that they are equal is a very deep and surprising fact, with implications not just for complexity theory but also for parts of pure mathematics, and in particular operator theory. RE is the class of recursively enumerable functions -- that is, Boolean functions fff for which there is an algorithm such that if f(x)=1f(x)=1f(x)=1, then the algorithm can establish this in finite time. Here there are no restrictions on how long the algorithm takes or how much memory it uses. The definition of MIP* is quite a lot less straightforward, but can be understood in a sequence of steps. First, the class P consists of Boolean functions that can be computed in polynomial time (in the length of the input). NP consists of Boolean functions f:{0,1}n→{0,1}f:\{0,1\}^n\to\{0,1\}f:{0,1}n→{0,1} such that if f(x)=1f(x)=1f(x)=1 then this fact can be _verified_ in polynomial time. That is, for each nnn there is some mmm that depends polynomially on nnn and a function g:{0,1}n+m→{0,1}g:\{0,1\}^{n+m}\to\{0,1\}g:{0,1}n+m→{0,1} in PPP such that for each xxx, f(x)=1f(x)=1f(x)=1 if and only if there exists y∈{0,1}my\in\{0,1\}^my∈{0,1}m with g(x,y)=1g(x,y)=1g(x,y)=1. We can think of such a yyy as a "certificate" that guarantees that f(x)=1f(x)=1f(x)=1. (For example, if fff detects whether there is a Hamilton cycle in a graph, ggg could be the function that takes a graph and an ordering on the vertices and outputs 1 if and only if that ordering defines a Hamilton cycle.) We can think of NP in a slightly different way as a collaboration between two agents, a powerful prover and a much less powerful verifier. They can collaborate as follows. The verifier presents the prover with a string xxx. The prover, unconstrained by any time or space limitations, responds with a string yyy. The verifier then calculates g(x,y)g(x,y)g(x,y). If g(x,y)=1g(x,y)=1g(x,y)=1 then f(x)=1f(x)=1f(x)=1 and otherwise f(x)=0f(x)=0f(x)=0. For this to work two properties of their protocol are needed. The first is _completeness_: that whenever f(x)=1f(x)=1f(x)=1 there is a suitable certificate yyy. The second is _soundness_: that whenever f(x)=0f(x)=0f(x)=0 there is no such certificate. We can imagine this as a situation where the prover always wants to convince the verifier that f(x)=1f(x)=1f(x)=1, regardless of whether that is actually true. If the protocol is both complete and sound, then in fact the verifier will always correctly determine the value of fff. To obtain the class IP (which stands for "interactive proof") we modify the above situation slightly, allowing the verifier access to a string of random bits, allowing communication between the verifier and prover to take place over several rounds, and requiring at the end only that that verifier is _almost_ certain that f(x)=1f(x)=1f(x)=1. Rather than give a formal definition, we present here an example due to Goldreich, Micali and Wigderson of a protocol that shows that non-isomorphism of graphs is in IP (which is not obvious, since while it is easy to see that graph isomorphism belongs to NP, there is no particular reason to suppose that graph _non_-isomorphism does). The idea is simple: the verifier takes two graphs GGG and HHH and sends to the prover a sequence (K1,…,Km)(K_1,\dots,K_m)(K1​,…,Km​) of graphs, where each KiK_iKi​ is obtained by randomly picking one of GGG and HHH and randomly permuting its vertices. The prover then sends back a 01-sequence x∈{0,1}mx\in\{0,1\}^mx∈{0,1}m. Finally, the verifier judges GGG and HHH to be non-isomorphic if xi=1x_i=1xi​=1 for all and only those iii for which KiK_iKi​ is isomorphic to GGG (which the verifier knows). If GGG and HHH are indeed non-isomorphic, the prover can ensure that the verifier will agree that this is the case, but otherwise the prover has no idea which KiK_iKi​ came from which graph and can therefore do so with probability only 2−m2^{-m}2−m. It turns out that IP is equal to the complexity class PSPACE, which consists of functions that can be computed with only a polynomial amount of memory (but with no restriction on time). This is already an indication of the power of interactive proofs. However, it turns out that with some simple modifications they can be made considerably more powerful. One modification is to have more than one prover and not to allow the provers to communicate. This makes it harder for the provers to fool the verifier if f(x)≠1f(x)\ne 1f(x)=1, since the verifier can be on the lookout for inconsistencies in their answers. The resulting class MIP (for "multiprover interactive proof") turns out to be equivalent to the complexity class NEXPTIME, which is like NP except that the verification is now allowed to take an exponential amount of time, so it is a huge class. Finally, we come to MIP*. Here quantum entanglement comes into play. Before the computation starts the provers are allowed to share entangled quantum bits, which have the potential to create correlations between their responses to the verifier. Potentially at least, this greatly enlarges the set of possible strategies for the provers, and therefore greatly enlarges the class of functions that can be computed. And this potential turns out to be realized: the statement that MIP*=RE is telling us the extraordinary fact that every recursively enumerable function belongs to MIP*. That is, if you are given a Turing machine and asked whether it halts, there is some protocol involving multiple provers using entangled bits such that if the Turing machine halts, the provers will convince the verifer of that fact, and otherwise the verifier will be almost certain that it does not halt. Note that there is no algorithm that will establish (in general) that a Turing machine does _not_ halt, but the fact that MIP*=RE tells us that if we are satisfied with being _almost_ certain that it does not halt, then for each instance of the problem there is an MIP* protocol that will give that to us. This paper concerns a particular problem from coding theory. A _linear code_ is a subspace C\mathcal CC of Fn\mathbb F^nFn for some finite field F\mathbb FF such that any two elements, or _codewords_, differ in at least ddd coordinates. (The bigger ddd is, the better the code.) Given such a code, the tensor code C⊗m\mathcal C^{\otimes m}C⊗m is defined to be the set of all functions g:[n]m→Fg:[n]^m\to\mathbb Fg:[n]m→F (where [n][n][n] denotes the set {1,2,…,n}\{1,2,\dots,n\}{1,2,…,n}) such that if you fix all but one coordinate, then the resulting restriction of ggg, regarded as an element of Fn\mathbb F^nFn in the obvious way, is an element of C\mathbb CC. The corresponding computational problem is to determine whether a given function ggg belongs to C⊗m\mathcal C^{\otimes m}C⊗m. Such codes are called _locally testable_ because there is a simple protocol that allows an interactive proof based on only local information. It works as follows. The verifier chooses a random element xxx of [n]m[n]^m[n]m, the prover responds with an element u∈Fu\in\mathbb Fu∈F, the verifier then chooses a random j∈[n]j\in[n]j∈[n], and the prover responds with a codeword www from C\mathcal CC. If wj=uw_j=uwj​=u, then the verifier judges ggg to belong to C⊗m\mathcal C^{\otimes m}C⊗m. Note that if ggg does indeed belong to C⊗m\mathcal C^{\otimes m}C⊗m, then all the prover has to do is choose the word obtained from the line of all points yyy such that yi=xiy_i=x_iyi​=xi​ when i≠ji\ne ji=j. Soundness of the protocol is less obvious (and requires a further technical condition on the code called interpolability) but follows quickly from a result of Babai, Fortnow and Lund. The main result of this paper can be thought of as saying that two interative provers cannot do significantly better for this problem if they are allowed to use entangled bits than if they are restricted to classical computation. For more details about tensor codes, this result, and how it relates to the MIP*=RE theorem, the extensive introduction to the paper itself is highly recommended.
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.