MIP* = RE

A multi-prover interactive proof pits a computationally bounded, coin-flipping verifier against several all-powerful but mutually isolated provers. The provers may rehearse a joint strategy beforehand, but once the verifier fires off its randomly chosen questions they cannot communicate. Classically this isolation is the whole source of power: cross-examining two provers who cannot coordinate their lies lets a polynomial-time verifier check statements of enormous length, the celebrated MIP=NEXP\mathrm{MIP}=\mathrm{NEXP} theorem. The starred class MIP∗\mathrm{MIP}^* changes one rule — the provers may share quantum entanglement, a double-edged sword. On one edge it lets them correlate answers in ways no classical script can reproduce, so it helps them cheat; on the other it lets the verifier test the shared quantum state itself with surgical precision, because only a particular entangled state reproduces certain answer statistics — so it helps the verifier catch them. For two decades nobody knew which edge won. Early results showed entanglement could destroy a classical protocol's soundness; then Ito and Vidick recovered the full classical power with NEXP⊆MIP∗\mathrm{NEXP}\subseteq\mathrm{MIP}^*, and Natarajan–Wright's NEEXP⊆MIP∗\mathrm{NEEXP}\subseteq\mathrm{MIP}^* revealed the class was strictly larger than NEXP\mathrm{NEXP}, powered by the verifier's ability to certify exponentially large entangled states with only polynomial communication. In January 2020 Ji, Natarajan, Vidick, Wright and Yuen reached the ceiling, and it was the highest imaginable: MIP∗=RE\mathrm{MIP}^*=\mathrm{RE}, the class of all recursively enumerable languages, which includes the undecidable Halting Problem. A statement about interrogating quantum provers turned out to settle a forty-year-old conjecture in the theory of von Neumann algebras.

Key takeaways
  • MIP∗\mathrm{MIP}^* is the class of languages a classical polynomial-time verifier can decide by interrogating two or more non-communicating provers who share unlimited quantum entanglement; the verifier accepts or rejects based on their answers to randomly chosen questions.
  • The 2020 theorem of Ji, Natarajan, Vidick, Wright and Yuen proves MIP∗=RE\mathrm{MIP}^*=\mathrm{RE}: entangled multi-prover proofs decide exactly the recursively enumerable languages — everything a Turing machine can accept, including the Halting Problem.
  • This is a colossal jump from classical MIP=NEXP\mathrm{MIP}=\mathrm{NEXP} and from single-prover QIP=PSPACE\mathrm{QIP}=\mathrm{PSPACE}: shared entanglement pushes verification power clean past the edge of computability.
  • The hard direction runs a gap-preserving compression: each round forces honest provers to hold an exponentially larger entangled state, so a finite nonlocal game can, via a self-referential fixed point, encode whether an arbitrary Turing machine halts.
  • As a corollary the theorem refutes Tsirelson's problem and Connes' 1976 embedding conjecture: the quantum correlation sets obey Cq‾≠Cqc\overline{C_q}\neq C_{qc}, so the tensor-product and commuting-operator models of two separated parties genuinely differ.
  • The engine underneath is rigidity, or self-testing: some games have an essentially unique optimal strategy — the CHSH game already pins down the maximally entangled pair and anticommuting observables from statistics alone.
  • Key idea: Entanglement lets a polynomial-time verifier certify, through rigidity and self-testing, that two isolated provers hold a specific exponentially large entangled state and measure it as instructed. Iterating a gap-preserving compression of that certification — each round checking an exponentially harder computation with only polynomially more talk — builds a finite nonlocal game whose entangled value is 1 exactly when a given Turing machine halts. Hence RE⊆MIP∗\mathrm{RE}\subseteq\mathrm{MIP}^*, and since proof systems are semidecidable, MIP∗=RE\mathrm{MIP}^*=\mathrm{RE}.
The core insight

Entanglement lets a polynomial-time verifier certify, via rigidity and self-testing, that two isolated provers hold a specific exponentially large entangled state and measure it as instructed; iterating a gap-preserving compression of that certification builds a finite nonlocal game whose entangled value encodes whether an arbitrary Turing machine halts, so MIP∗=RE\mathrm{MIP}^*=\mathrm{RE}.

Where this lives today

The theorem is only a few years old and its aftershocks are still spreading across three fields. In operator algebras it is, to date, the only known route to refuting Connes' embedding conjecture, and a small industry now works to translate the computer-science proof into a self-contained mathematical one. In quantum complexity, researchers are compressing the compression: the original argument runs past one hundred and fifty pages, and simplified proofs and clean expositions of the introspection and Pauli-braiding tests are active targets. In quantum cryptography the same rigidity that powers the theorem underlies self-testing, certified randomness, and delegated verification of untrusted quantum devices — the theorem marks the outer limit of what nonlocal-game tests can certify and shows that no finite test certifies everything, because the value landscape is uncomputable. Most concretely, it kills a physicists' hope: because deciding ω∗(G)=1\omega^*(G)=1 is as hard as halting, no general algorithm approximates the maximum quantum violation of an arbitrary Bell inequality to fixed accuracy — a sharp contrast with the commuting-operator value, which the NPA hierarchy does converge to from above.

The physical picture

Picture two suspects questioned in separate rooms. A clever detective who cannot let them coordinate can still verify astonishing claims by cross-checking their stories — the classical intuition behind MIP=NEXP\mathrm{MIP}=\mathrm{NEXP}. Now hand the suspects a supply of entangled particles they each measure privately. The naive worry is that this only helps them collude; the deep surprise of MIP∗\mathrm{MIP}^* is that it helps the detective more, because certain question-and-answer patterns can be produced only if the suspects genuinely hold one particular entangled state and measure it one particular way. So the detective can interrogate not just their story but the structure of their shared resource, and that structure can be made exponentially rich while the interrogation stays short. The first figure shows the setup and the number that makes it non-classical.

Figure
A two-prover nonlocal game: the verifier samples questions x and y, sends one to each isolated prover, and checks the answers a and b against a fixed predicate while Alice and Bob share entanglement but cannot talk. For the CHSH game the best classical strategy wins 3/4 = 0.75 of the time, but a shared Bell pair raises the winning probability to 1/2 + 1/(2√2) ≈ 0.8536
A nonlocal game: isolate the provers, hand them entanglement, cross-examine Verifier poly-time, random Alice prover 1 Bob prover 2 question x answer a question y answer b shared entangled state |ψ⟩ ∈ ℋ_A ⊗ ℋ_B (no communication) CHSH classical ω = 3/4 = 0.75 entangled ω* = 1/2 + 1/(2√2) ≈ 0.8536

The reason entanglement is so powerful for the verifier is rigidity: the largest achievable value of a game like CHSH forces, up to a local change of basis, one unique state and one unique pair of measurements. That microscopic fact scales. By stitching rigidity tests together the verifier can force the provers to hold an entangled state of exponential dimension and answer questions about a computation exponentially longer than the questions themselves — and, feeding the verifier a compressed copy of its own description, a finite game unfolds an unbounded computation. The second figure is the ladder this climbs, and the undecidable gap it lands on.

Figure
The complexity ladder that gap-preserving compression climbs: classical two-prover proofs reach only NEXP, but entangled provers reach NEEXP and then every level up to RE. Compression sends a verifier V to a verifier V′ of size poly(log T(V)), and the entangled value obeys ω(G_M) = 1 when the machine M halts and ω(G_M) ≤ 1/2 otherwise, so the value is undecidable and the correlation sets satisfy closure of C_q ≠ C_qc
Compression climbs the ladder and lands on an undecidable value RE = MIP* (JNVWY 2020) NEEXP ⊆ MIP* (Natarajan–Wright 2019) NEXP = MIP (Babai–Fortnow–Lund 1991) PSPACE = QIP single-prover quantum proofs The engine compression: V ↦ V′ |V′| = poly(log T) each step: harder check, same-size talk The gap ω*(G_M) = 1 if M halts ω*(G_M) ≤ 1/2 if M runs forever value undecidable ⇒ closure C_q ≠ C_qc Halting Problem ≤ deciding ω*(G) = 1, so no algorithm approximates the entangled value.

The core equations

The whole subject hangs on one line that hides a proof of over one hundred and fifty pages. State the theorem first; everything after is its definition, its consequence, or the machinery that makes it true.

MIP∗=RE(1)\mathrm{MIP}^* = \mathrm{RE} \qquad (1)

where: MIP∗\mathrm{MIP}^* — languages decided by a classical polynomial-time verifier and two entangled, non-communicating provers with a completeness–soundness gap c−s≥1/polyc-s\ge 1/\mathrm{poly}; RE\mathrm{RE} — the recursively enumerable languages accepted by some Turing machine, a class whose acceptance is only semidecidable and whose complete problem is the Halting Problem. Reading: entangled multi-prover proofs verify every language any computer can even in principle accept. Everything the verifier does is scored by the entangled value of a nonlocal game — the best success probability over all finite-dimensional shared states and local measurements. This is the quantity the whole theorem is secretly about.

ω∗(G)=sup⁡∣ψ⟩∈HA⊗HB{Axa},{Byb}∑x,yπ(x,y)∑a,bV(a,b ∣ x,y) ⟨ψ∣ Axa⊗Byb ∣ψ⟩(2)\omega^*(G) = \sup_{\substack{|\psi\rangle\in\mathcal H_A\otimes\mathcal H_B \\ \{A_x^a\},\,\{B_y^b\}}} \sum_{x,y}\pi(x,y)\sum_{a,b} V(a,b\,|\,x,y)\,\langle\psi|\,A_x^a\otimes B_y^b\,|\psi\rangle \qquad (2)

where: π(x,y)\pi(x,y) — the distribution the verifier draws questions from, xx to Alice and yy to Bob; V(a,b ∣ x,y)V(a,b\,|\,x,y) — the predicate, 11 if the answers are accepted and 00 otherwise; ∣ψ⟩|\psi\rangle — the shared entangled state, of finite but unbounded dimension; Axa,BybA_x^a,B_y^b — POVM elements with ∑aAxa=1\sum_a A_x^a=\mathbb 1. Reading: it is a supremum, not a maximum — for some games no finite-dimensional strategy attains the value, and that single word is where the operator-algebra drama lives. A language belongs to MIP∗\mathrm{MIP}^* when its yes- and no-instances are separated by a promise gap in this value, which the verifier turns into a game in polynomial time. The verifier itself stays classical and efficient; all the quantum power lives in the provers' shared state.

L∈MIP∗[c,s]  ⟺  (x∈L⇒ω∗(Gx)≥c)  ∧  (x∉L⇒ω∗(Gx)≤s)(3)L\in\mathrm{MIP}^*[c,s]\iff\big(x\in L\Rightarrow\omega^*(G_x)\ge c\big)\;\wedge\;\big(x\notin L\Rightarrow\omega^*(G_x)\le s\big) \qquad (3)

where: GxG_x — the nonlocal game built in poly(∣x∣)\mathrm{poly}(|x|) time from the input; cc — completeness, guaranteed by honest provers when x∈Lx\in L; ss — soundness, the ceiling on any strategy when x∉Lx\notin L; c−s≥1/poly(∣x∣)c-s\ge 1/\mathrm{poly}(|x|) — the promise gap, amplifiable to c=1,  s≤12c=1,\;s\le\tfrac12. Reading: the verifier never learns why the value is high, only that the gap decides membership. The smallest nontrivial nonlocal game, CHSH, already carries a hard number that separates classical from quantum. It anchors every rigidity argument to follow, because the full construction is built from copies of this one game.

ω(CHSH)=34,ω∗(CHSH)=12+122=cos⁡2 ⁣π8≈0.8536(4)\omega(\mathrm{CHSH})=\tfrac34,\qquad \omega^*(\mathrm{CHSH})=\tfrac12+\tfrac{1}{2\sqrt2}=\cos^2\!\tfrac{\pi}{8}\approx 0.8536 \qquad (4)

where: ω\omega — the best classical winning probability; ω∗\omega^* — the best entangled winning probability, Tsirelson's bound as a probability; the Bell-operator value is ⟨B⟩=22≈2.8284\langle\mathcal B\rangle=2\sqrt2\approx2.8284. Reading: entanglement buys an unconditional advantage of ≈0.1036\approx0.1036, and the strategy achieving it is essentially unique — the seed of self-testing. The theorem's fallout for mathematics is the separation of the two ways to model "spatially separated subsystems," which prior to 2020 was Tsirelson's open problem. The two correlation sets nest by construction; the only question was ever whether the outer containment is strict.

Cq⊆Cq‾⊆Cqc,Cq‾≠Cqc(5)C_q\subseteq\overline{C_q}\subseteq C_{qc},\qquad \overline{C_q}\neq C_{qc} \qquad (5)

where: CqC_q — correlations p(a,b∣x,y)=⟨ψ∣Axa⊗Byb∣ψ⟩p(a,b|x,y)=\langle\psi|A_x^a\otimes B_y^b|\psi\rangle from finite-dimensional tensor-product strategies; Cq‾\overline{C_q} — its closure; CqcC_{qc} — correlations from commuting-operator strategies on a single Hilbert space with [Axa,Byb]=0[A_x^a,B_y^b]=0. Reading: the two models coincide in finite dimension, but MIP∗=RE\mathrm{MIP}^*=\mathrm{RE} forces them apart in the limit, which through a chain of equivalences refutes Connes' embedding conjecture. The hard inclusion is powered by gap-preserving compression, a polynomial-time transformation that shrinks a verifier while forcing the provers to shoulder the work it dropped. It is the one genuinely new ingredient of the 2020 proof, the piece the whole field had been building toward.

Compress:  V⟼V′with∣V′∣=poly(log⁡T(V)),ω∗(GV′)=1  ⟺  ω∗(GV)=1(6)\mathrm{Compress}:\;V\longmapsto V'\quad\text{with}\quad |V'|=\mathrm{poly}\big(\log T(V)\big),\qquad \omega^*(G_{V'})=1\iff\omega^*(G_V)=1 \qquad (6)

where: VV — a verifier whose game runs in time T(V)T(V); V′V' — the compressed verifier, only polylogarithmic in VV's runtime, whose game makes the provers simulate VV and answer about a low-degree encoding of its transcript, policed by rigidity tests; the gap behaviour (=1=1 versus ≤12\le\tfrac12) is preserved. Reading: the verifier's description shrinks exponentially relative to the computation it verifies — the shrink is what lets a verifier be fed its own code. Feeding compression to itself through Kleene's recursion theorem produces a finite game that decides halting, which is the entire content of RE⊆MIP∗\mathrm{RE}\subseteq\mathrm{MIP}^*. The move is the same self-reference that underlies quines, now applied to a nonlocal game rather than a program.

V⋆=Compress(V⋆)  ⟹  ω∗(GV⋆)=1  ⟺  M halts(7)V^\star=\mathrm{Compress}(V^\star)\;\Longrightarrow\;\omega^*(G_{V^\star})=1\iff M\text{ halts} \qquad (7)

where: V⋆V^\star — a fixed point of the compression map, a verifier that effectively references its own compressed code; MM — the Turing machine wired into the recursion's base case. Reading: each query to GV⋆G_{V^\star} unfolds one more level of an unbounded nested verification without enlarging the finite description, so the value is 11 exactly when the unfolding "bottoms out," which happens iff MM halts.

Derivation AWhy entangled proofs can be no more than recursively enumerable

The goal of this derivation is the easy half of the theorem, MIP∗⊆RE\mathrm{MIP}^*\subseteq\mathrm{RE}, which needs none of the compression machinery and explains why RE\mathrm{RE} is the natural ceiling rather than something larger. We show that membership is semidecidable — a procedure that halts and accepts on every yes-instance and never accepts on a no-instance. The engine is that the entangled value is a supremum approached from below, so a brute-force search over finite-dimensional strategies of growing size eventually witnesses any achievable value. Assume perfect completeness c=1c=1 and soundness s≤12s\le\tfrac12, which amplification guarantees.

Step 1. On input xx the verifier's polynomial-time description yields a concrete nonlocal game GxG_x with the promise ω∗(Gx)=1\omega^*(G_x)=1 if x∈Lx\in L and ω∗(Gx)≤12\omega^*(G_x)\le\tfrac12 if x∉Lx\notin L. Why: the verifier is a fixed poly-time algorithm, so the game is fully computable from xx — nothing is hidden except the provers' strategies.

Step 2. Enumerate finite-dimensional entangled strategies for dimension d=1,2,3,…d=1,2,3,\dots, discretizing states and measurements to accuracy ε\varepsilon, and evaluate the winning probability of each. These values converge to ω∗(Gx)\omega^*(G_x) from below because higher dimension can only help the supremum. Why: the value is a sup over a nested family, so any achievable value is reached up to ε\varepsilon at some finite dd.

Step 3. Accept the moment some strategy scores above 12\tfrac12. If x∈Lx\in L the value is 11, so a finite dd crosses 12\tfrac12 and the search halts and accepts; if x∉Lx\notin L no strategy ever exceeds 12\tfrac12, so the search runs forever. Why: this asymmetry — halt-and-accept on yes, silent-forever on no — is exactly the definition of a recursively enumerable set.

Step 4. Therefore the language is accepted by a Turing machine, so MIP∗⊆RE\mathrm{MIP}^*\subseteq\mathrm{RE}, and the whole theorem reduces to the reverse inclusion. Why: no compression is needed for this half; the depth is entirely in showing that this ceiling is actually reached.

Go deeper · Derivation B · 2 minThe CHSH game, Tsirelson's bound, and the birth of rigidity
Derivation BThe CHSH game, Tsirelson's bound, and the birth of rigidity

This derivation computes the exact classical and quantum values of the CHSH game and shows that the quantum optimum is rigid — achievable only by one state and one set of observables up to a local isometry. The point is the rigidity, not the small numerical gap, because self-testing scaled and composed is precisely what lets the verifier certify exponentially large entangled states inside the full theorem. The game: the verifier sends uniform bits x,y∈{0,1}x,y\in\{0,1\}, receives bits a,b∈{0,1}a,b\in\{0,1\}, and the provers win iff a⊕b=x∧ya\oplus b=x\wedge y.

Step 1. Over deterministic strategies a=f(x)a=f(x), b=g(y)b=g(y) the win condition f(x)⊕g(y)=x∧yf(x)\oplus g(y)=x\wedge y can be satisfied for at most 33 of the 44 equally likely question pairs, because the four constraints are jointly unsatisfiable; shared randomness is a convex mixture of deterministic strategies and cannot beat their maximum. Hence ω(CHSH)=3/4\omega(\mathrm{CHSH})=3/4. Why: classical provers are just a lookup table fixed in advance, and no table clears all four parity constraints at once.

Step 2. Let the provers share the Bell state ∣ψ⟩=12(∣00⟩+∣11⟩)|\psi\rangle=\tfrac1{\sqrt2}(|00\rangle+|11\rangle). Alice measures observables A0=ZA_0=Z, A1=XA_1=X; Bob measures B0=Z+X2B_0=\tfrac{Z+X}{\sqrt2}, B1=Z−X2B_1=\tfrac{Z-X}{\sqrt2}, each with eigenvalues ±1\pm1. Why: mapping outcome bits to ±1\pm1 signs turns the parity win condition into a correlation, and these particular axes sit at the 45∘45^\circ angles that maximize it.

Step 3. Form the Bell operator B=A0B0+A0B1+A1B0−A1B1\mathcal B=A_0B_0+A_0B_1+A_1B_0-A_1B_1. Since Ai2=Bj2=1A_i^2=B_j^2=\mathbb 1, one finds B2=4 1−[A0,A1]⊗[B0,B1]\mathcal B^2=4\,\mathbb 1-[A_0,A_1]\otimes[B_0,B_1], and each commutator has norm at most 22, so ∥B2∥≤8\|\mathcal B^2\|\le 8 and ∥B∥≤22\|\mathcal B\|\le 2\sqrt2. The chosen strategy attains ⟨ψ∣B∣ψ⟩=22≈2.8284\langle\psi|\mathcal B|\psi\rangle=2\sqrt2\approx2.8284, Tsirelson's bound. Why: the commutator term is the purely quantum piece; classically the observables commute and the bound collapses back to 22, the classical Bell limit.

Step 4. Convert the Bell value to a winning probability with ω∗=12+18⟨B⟩\omega^*=\tfrac12+\tfrac18\langle\mathcal B\rangle. At the Tsirelson value ω∗=12+228=12+24=12+122=cos⁡2π8≈0.8536\omega^*=\tfrac12+\tfrac{2\sqrt2}{8}=\tfrac12+\tfrac{\sqrt2}{4}=\tfrac12+\tfrac{1}{2\sqrt2}=\cos^2\tfrac{\pi}{8}\approx0.8536, beating 3/43/4 by ≈0.1036\approx0.1036. Why: the coefficient is 1/81/8, not 1/41/4 — the four question pairs each carry weight 1/41/4 and the correlation-to-probability map contributes a further factor 1/21/2, so the probability stays safely below 11.

Step 5. Rigidity: any strategy reaching 222\sqrt2 must, up to a local isometry, use the maximally entangled pair and anticommuting observables {X,Z}\{X,Z\} on each side. The value alone pins down the state and the measurements. Why: this self-testing is the microscopic mechanism the whole theorem scales up — from certifying one Bell pair to certifying an exponentially large entangled state with only polynomial communication. *Note: the anticommutation {X,Z}=0\{X,Z\}=0 is what gives B2=4 1−[A0,A1][B0,B1]\mathcal B^2=4\,\mathbb 1-[A_0,A_1][B_0,B_1], and the numerical check 12+18(22)=12+122=0.8536\tfrac12+\tfrac18(2\sqrt2)=\tfrac12+\tfrac{1}{2\sqrt2}=0.8536 confirms the winning probability.*

Go deeper · Derivation C · 2 minFrom compression and self-reference to undecidability
Derivation CFrom compression and self-reference to undecidability

Here we assemble the hard inclusion RE⊆MIP∗\mathrm{RE}\subseteq\mathrm{MIP}^* by combining gap-preserving compression with Kleene's recursion theorem to manufacture, for any Turing machine MM, a finite nonlocal game GMG_M whose entangled value is 11 exactly when MM halts and at most 12\tfrac12 otherwise. Because halting is undecidable, this proves the entangled value uncomputable and, with the easy inclusion, closes the theorem. The construction is a fixed point: a game that plays a compressed copy of itself, wired so unbounded self-application succeeds precisely when MM terminates.

Step 1. Establish the compression primitive: a polynomial-time map sending a verifier VV with runtime T(V)T(V) to V′V' with ∣V′∣=poly(log⁡T(V))|V'|=\mathrm{poly}(\log T(V)), such that GV′G_{V'} has the same gap behaviour as GVG_V. Internally GV′G_{V'} forces the provers to share an exponentially larger entangled state and to answer questions about a low-degree encoding of VV's transcript, with consistency enforced by rigidity tests such as Pauli braiding and question introspection. Why: introspection lets the verifier ask about questions it is too small to write down, and rigidity guarantees the provers cannot fake the exponentially large state they claim to hold.

Step 2. Because compression only mildly enlarges VV, a verifier can accept its own compressed description as input. Define a verifier that, given code ⟨W⟩\langle W\rangle, computes Compress(W)\mathrm{Compress}(W) and plays the resulting game. Why: the polylogarithmic size bound is exactly the room needed to fit a self-reference — a verifier that would double in size each round could never close the loop.

Step 3. By Kleene's recursion theorem there is a V⋆V^\star satisfying GV⋆=GCompress(V⋆)G_{V^\star}=G_{\mathrm{Compress}(V^\star)}. Each query to GV⋆G_{V^\star} therefore peels off one more level of an unbounded nested verification while the finite description never grows. Why: the recursion theorem manufactures a genuine fixed point of an effective transformation, turning "the game plays a compressed copy of itself" from a wish into a construction.

Step 4. Hard-wire MM into the base case so the infinite unfolding attains value 11 precisely when MM's computation halts, and is capped at 12\tfrac12 otherwise. Completeness uses honest provers holding a growing, in the limit infinite-dimensional, entangled state; soundness uses rigidity to bound every cheating strategy below the cap. Why: the two-sided gap is what makes the value a faithful yes/no encoding of halting rather than a smeared-out quantity.

Step 5. The Halting Problem now many-one reduces to deciding ω∗(Gx)=1\omega^*(G_x)=1; since it is RE\mathrm{RE}-complete, every RE\mathrm{RE} language reduces likewise, giving RE⊆MIP∗\mathrm{RE}\subseteq\mathrm{MIP}^*. With Derivation A, MIP∗=RE\mathrm{MIP}^*=\mathrm{RE} and the entangled value is undecidable. Why: undecidability of the value is the theorem's sharpest edge — it is what forces the correlation sets apart and refutes Connes.

Limiting cases

Reading MIP∗\mathrm{MIP}^* against its neighbours shows exactly which resource does the work — the second prover, the entanglement, and the infinite dimension are each load-bearing.

CaseResultMeaning
No entanglement (classical MIP)MIP=NEXP\mathrm{MIP}=\mathrm{NEXP}Babai–Fortnow–Lund: two non-communicating classical provers with a poly-time verifier decide nondeterministic exponential time. Entanglement strictly increases power, since NEXP⊊RE\mathrm{NEXP}\subsetneq\mathrm{RE}.
Single prover, quantum messagesQIP=PSPACE\mathrm{QIP}=\mathrm{PSPACE}One prover trading quantum messages with the verifier yields only PSPACE; the leap to RE requires at least two isolated provers who share entanglement.
Commuting-operator modelMIPco⊆coRE\mathrm{MIP}^{co}\subseteq\mathrm{coRE}With commuting-operator strategies the value is semidecidable from above via the NPA hierarchy. Equality with MIP∗\mathrm{MIP}^* would force decidability — impossible — so the two models differ.
Halting instance (completeness)ω∗(GM)=1  ⟺  M\omega^*(G_M)=1\iff M haltsHonest provers with a growing, possibly infinite-dimensional entangled state win GMG_M with probability tending to 11; if MM never halts the value is capped at 12\tfrac12.
Provers and roundsMIP∗[2,1]=MIP∗=RE\mathrm{MIP}^*[2,1]=\mathrm{MIP}^*=\mathrm{RE}Two provers and a single round already suffice; the full power of RE needs no extra provers or interaction rounds.

Worked examples

1 · The CHSH advantage, worked to the last digit (confidence builder)

Compute the exact classical and entangled winning probabilities of the CHSH game, and the size of the quantum advantage, from the Bell operator.

Step 1. Classical ceiling. The four question pairs (x,y)∈{0,1}2(x,y)\in\{0,1\}^2 demand a⊕ba\oplus b equal to 0,0,0,10,0,0,1 respectively. Any fixed pair of answer functions satisfies at most three of these — the AND being true only for (1,1)(1,1) is the obstruction — so the best classical winning probability is ω=3/4=0.75\omega=3/4=\mathbf{0.75}.

Step 2. Bell value of the quantum strategy. With the Bell pair and the observables A0=Z,  A1=X,  B0=Z+X2,  B1=Z−X2A_0=Z,\;A_1=X,\;B_0=\tfrac{Z+X}{\sqrt2},\;B_1=\tfrac{Z-X}{\sqrt2}, each of the four correlators equals ⟨ψ∣AiBj∣ψ⟩=±12\langle\psi|A_iB_j|\psi\rangle=\pm\tfrac{1}{\sqrt2}, and the signed sum gives ⟨B⟩=4⋅12=22≈2.8284\langle\mathcal B\rangle=4\cdot\tfrac{1}{\sqrt2}=2\sqrt2\approx\mathbf{2.8284}, saturating Tsirelson's bound ∥B∥≤22\|\mathcal B\|\le2\sqrt2.

Step 3. Winning probability. Apply ω∗=12+18⟨B⟩=12+228=12+24\omega^*=\tfrac12+\tfrac18\langle\mathcal B\rangle=\tfrac12+\tfrac{2\sqrt2}{8}=\tfrac12+\tfrac{\sqrt2}{4}. Numerically 24=0.35355\tfrac{\sqrt2}{4}=0.35355, so ω∗=0.85355=cos⁡2π8\omega^*=\mathbf{0.85355}=\cos^2\tfrac{\pi}{8}, and equivalently 12+122\tfrac12+\tfrac{1}{2\sqrt2}.

Step 4. The advantage. The entangled provers beat the classical ceiling by 0.85355−0.75=0.103550.85355-0.75=\mathbf{0.10355} — an unconditional gap achievable with a single Bell pair and no communication. Classical 3/4 = 0.75, entangled 1/2 + 1/(2√2) ≈ 0.8536, advantage ≈ 0.1036, and the optimal strategy is rigid.

2 · A pseudo-telepathy game: the Mermin–Peres magic square

Show a nonlocal game whose entangled value is exactly 1 while its classical value is strictly below 1, illustrating the completeness regime the halting construction exploits.

Step 1. The setup. Fill a 3×33\times3 grid with entries in {+1,−1}\{+1,-1\} so that every row multiplies to +1+1 and every column multiplies to −1-1. Multiplying all nine entries row-wise gives +1+1 but column-wise gives −1-1 — a parity contradiction, so no single global assignment satisfies all six constraints.

Step 2. The game. The verifier sends Alice a random row and Bob a random column; Alice returns three signs with the required row product, Bob returns three signs with the required column product, and they win iff their entries agree at the cell where the chosen row and column cross. Because no consistent global grid exists, the best classical strategy wins at most 88 of the 99 row–column pairs, so ω=8/9≈0.889\omega=8/9\approx\mathbf{0.889}.

Step 3. The quantum strategy. Sharing two Bell pairs, Alice and Bob assign each cell a two-qubit Pauli observable from a fixed magic-square array whose rows and columns commute and multiply to +1+\mathbb 1 along rows and −1-\mathbb 1 along columns. Measuring the requested line yields signs that satisfy the line constraint and always agree at the intersection cell, so they win every time: ω∗=1\omega^*=\mathbf{1}.

Step 4. The lesson. Entanglement lifts an impossible-to-win-perfectly classical game to one won with certainty. This "value exactly 1 if a consistency condition holds, bounded below 1 if it fails" template is the local motif that, iterated by compression, becomes "value 1 iff MM halts." Classical 8/9 ≈ 0.889, entangled 1 exactly — no classical perfect strategy, but a quantum one.

Physics of the portrait

The bound at the heart of every rigidity argument bears one name, and its author posed the very question this theorem answered — dying, as it happened, in the same month the answer appeared.

Origins · 1 minBoris Tsirelson and how this was discovered
BT
Boris Tsirelson
1950–2020 · quantum nonlocality, the Tsirelson bound, and Tsirelson's problem

Boris Semyonovich Tsirelson was born in Leningrad in 1950 and emigrated to Israel in 1991, spending his career at Tel Aviv University — better known to many mathematicians for deep work in probability and the "Tsirelson space" of Banach-space theory than for the physics that made his name famous in quantum information. In 1980, sharpening Bell's inequality, he proved that CHSH quantum correlations cannot exceed 222\sqrt2, the ceiling now universally called Tsirelson's bound; it is the value Derivation B saturates and the reason the quantum winning probability lands at cos⁡2π8≈0.8536\cos^2\tfrac{\pi}{8}\approx0.8536 rather than 11. More consequentially, in the early 1990s he asked whether the tensor-product and commuting-operator models of two separated observers yield the same achievable correlations. That question became Tsirelson's problem, and through work of Fritz, Junge and collaborators, and Ozawa it was tied to Connes' 1976 embedding conjecture. When Ji, Natarajan, Vidick, Wright and Yuen posted MIP∗=RE\mathrm{MIP}^*=\mathrm{RE} on 13 January 2020, they answered it in the negative: Cq‾≠Cqc\overline{C_q}\neq C_{qc}. Tsirelson died on 21 January 2020, days after the preprint appeared, having lived just long enough to see a complexity-theoretic proof settle the problem he had opened.

History
1980
— Tsirelson proves the quantum bound 2√2 on CHSH correlations
1988
— Ben-Or, Goldwasser, Kilian and Wigderson introduce multi-prover interactive proofs
1991
— Babai, Fortnow and Lund prove MIP = NEXP
2012
— Ito and Vidick show NEXP is contained in MIP*
2020
— Ji, Natarajan, Vidick, Wright and Yuen prove MIP* = RE

Going further

References. Ji, Natarajan, Vidick, Wright, Yuen, "MIP = RE", arXiv:2001.04383 (2020) · Babai, Fortnow, Lund, "Non-deterministic exponential time has two-prover interactive protocols", Comput. Complexity 1 (1991) · Ito, Vidick, "A multi-prover interactive proof for NEXP sound against entangled provers", FOCS 2012 · Natarajan, Wright, "NEEXP ⊆ MIP", FOCS 2019 · Ben-Or, Goldwasser, Kilian, Wigderson, "Multi-prover interactive proofs", STOC 1988 · Jain, Ji, Upadhyay, Watrous, "QIP = PSPACE", J. ACM 58 (2011) · Tsirelson, "Quantum generalizations of Bell's inequality", Lett. Math. Phys. 4 (1980) · Cleve, Høyer, Toner, Watrous, "Consequences and limits of nonlocal strategies", CCC 2004 · Junge, Navascués, Palazuelos, Pérez-García, Scholz, Werner, "Connes' embedding problem and Tsirelson's problem", J. Math. Phys. 52 (2011) · Watrous, "The Theory of Quantum Information", Cambridge University Press (2018). Key numerical anchors: CHSH classical value 3/43/4, Tsirelson bound 222\sqrt2, and winning probability 12+18(22)=12+122=cos⁡2π8≈0.8536\tfrac12+\tfrac18(2\sqrt2)=\tfrac12+\tfrac{1}{2\sqrt2}=\cos^2\tfrac\pi8\approx0.8536; magic-square values, classical 8/98/9 and quantum 11; the chain Cq⊆Cq‾⊆CqcC_q\subseteq\overline{C_q}\subseteq C_{qc}; and MIP=NEXP\mathrm{MIP}=\mathrm{NEXP}, QIP=PSPACE\mathrm{QIP}=\mathrm{PSPACE}, and the compression-plus-recursion structure of MIP∗=RE\mathrm{MIP}^*=\mathrm{RE}. The winning-probability coefficient is 1/81/8, so no value exceeds 11.

Prerequisites. Quantum Interactive Proofs (QIP) · QIP = PSPACE · Quantum Merlin-Arthur (QMA) · BQP versus P, NP, and PSPACE. Leads to. Connes Embedding Problem · Nonlocal Games and Tsirelson's Bound · Self-Testing and Rigidity.

Ask the tutor: Ask me to work the CHSH Bell value out operator by operator, to trace how compression plus Kleene's recursion theorem plants a Turing machine into a finite game, or to unpack the RE-versus-coRE squeeze that refutes Connes' embedding conjecture.

Does MIP* = RE mean quantum provers can solve the Halting Problem?

No. Nobody — not the verifier, not the provers — ever computes whether a machine halts. The theorem says only that when MM halts there exists a perfect entangled strategy for GMG_M, and when MM runs forever every strategy is capped at 12\tfrac12. The undecidability sits in the abstract value ω∗(GM)\omega^*(G_M), not in any physical protocol you could run. In fact the winning strategy in the halting case needs a limiting infinite-dimensional state no device can hold; the provers only approach it. The verifier just runs a poly-time protocol whose acceptance probability encodes the answer without anyone learning it.

What is a nonlocal game, concretely?

It is a cooperative game between two players, Alice and Bob, and a referee. The referee samples a pair of questions from a fixed distribution and sends one to each; the players, who agreed on a strategy beforehand but cannot now communicate, each reply with an answer; the referee applies a fixed predicate to the questions and answers and declares a win or loss. With only classical shared randomness the best they achieve is the classical value; sharing entangled particles they can sometimes do strictly better, and that best is the entangled value ω∗\omega^*. CHSH and the magic square are the two smallest interesting examples, and every MIP∗\mathrm{MIP}^* protocol is ultimately a family of such games.

Which direction of the theorem is the hard one?

The inclusion MIP∗⊆RE\mathrm{MIP}^*\subseteq\mathrm{RE} is nearly free: enumerate finite-dimensional strategies of growing size and accept the moment one crosses the completeness threshold — a semidecision procedure, because the value is a supremum approached from below. All the depth is in RE⊆MIP∗\mathrm{RE}\subseteq\mathrm{MIP}^*. That direction requires the gap-preserving compression that shrinks a verifier to polylogarithmic size while forcing the provers to simulate the work it dropped, the rigidity and introspection tests that keep the provers honest about an exponentially large state, and Kleene's recursion theorem to close a self-referential loop so that a finite game encodes an unbounded halting computation. Compression is the genuinely new engine; everything else in the field had been building toward it since Ito–Vidick.

How does a statement about provers refute Connes' embedding conjecture?

Through a chain of equivalences. Connes' 1976 conjecture asked whether every separable type II1_1 von Neumann factor embeds, in trace, into an ultrapower of the hyperfinite II1_1 factor — loosely, whether such traces are approximable by finite matrices. Work of Fritz, of Junge and collaborators, and of Ozawa showed this is equivalent to Tsirelson's problem, whether the tensor-product correlation set's closure Cq‾\overline{C_q} equals the commuting-operator set CqcC_{qc}. Now the complexity input bites: the tensor-product value is approximable from below (RE) and the commuting-operator value from above (coRE), so if the two sets were equal the common value would be decidable. But MIP∗=RE\mathrm{MIP}^*=\mathrm{RE} makes deciding it as hard as halting — undecidable. Hence Cq‾≠Cqc\overline{C_q}\neq C_{qc}, and Connes' conjecture is false.

What is compression really doing?

Compression is a transformation on verifiers. Given a verifier VV whose game takes time T(V)T(V) to check, it produces a new verifier V′V' whose description is only poly(log⁡T(V))\mathrm{poly}(\log T(V)) long — exponentially smaller than the computation it certifies — but whose game has the same yes/no value behaviour. It buys this by offloading work onto the provers: V′V' makes them share an exponentially larger entangled state and answer questions about an encoded transcript of VV's computation, while rigidity tests (Pauli braiding, introspection) prevent them from lying about that state. The payoff is self-reference: because V′V' is so much smaller than the computation, a verifier can be handed its own compressed code, and a fixed point of that map is a finite game that unfolds an unbounded computation one query at a time.

Can any of this be tested in a laboratory?

Not the theorem itself — its completeness case needs an idealized infinite-dimensional state — but its building blocks are thoroughly experimental. CHSH violations reaching toward the 222\sqrt2 bound are routine in loophole-free Bell tests with photons, atoms, and superconducting qubits, and self-testing of Bell pairs and of small magic-square-style configurations has been demonstrated. What the laboratory cannot do is climb the compression ladder to infinity, so the halting encoding stays a mathematical object. The practical fallout is instead negative and firm: because the general entangled value is uncomputable, there is no algorithm a physicist can run to find the exact maximum quantum violation of an arbitrary Bell inequality, which reshapes how such optimizations are approached.

Before this