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 theorem. The starred class 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 , and Natarajan–Wright's revealed the class was strictly larger than , 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: , 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.
- 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 : 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 and from single-prover : 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 , 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 , and since proof systems are semidecidable, .
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 .
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 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 . 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 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.
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.
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.
where: — languages decided by a classical polynomial-time verifier and two entangled, non-communicating provers with a completeness–soundness gap ; — 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.
where: — the distribution the verifier draws questions from, to Alice and to Bob; — the predicate, if the answers are accepted and otherwise; — the shared entangled state, of finite but unbounded dimension; — POVM elements with . 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 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.
where: — the nonlocal game built in time from the input; — completeness, guaranteed by honest provers when ; — soundness, the ceiling on any strategy when ; — the promise gap, amplifiable to . 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.
where: — the best classical winning probability; — the best entangled winning probability, Tsirelson's bound as a probability; the Bell-operator value is . Reading: entanglement buys an unconditional advantage of , 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.
where: — correlations from finite-dimensional tensor-product strategies; — its closure; — correlations from commuting-operator strategies on a single Hilbert space with . Reading: the two models coincide in finite dimension, but 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.
where: — a verifier whose game runs in time ; — the compressed verifier, only polylogarithmic in 's runtime, whose game makes the provers simulate and answer about a low-degree encoding of its transcript, policed by rigidity tests; the gap behaviour ( versus ) 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 . The move is the same self-reference that underlies quines, now applied to a nonlocal game rather than a program.
where: — a fixed point of the compression map, a verifier that effectively references its own compressed code; — the Turing machine wired into the recursion's base case. Reading: each query to unfolds one more level of an unbounded nested verification without enlarging the finite description, so the value is exactly when the unfolding "bottoms out," which happens iff halts.
The goal of this derivation is the easy half of the theorem, , which needs none of the compression machinery and explains why 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 and soundness , which amplification guarantees.
Step 1. On input the verifier's polynomial-time description yields a concrete nonlocal game with the promise if and if . Why: the verifier is a fixed poly-time algorithm, so the game is fully computable from — nothing is hidden except the provers' strategies.
Step 2. Enumerate finite-dimensional entangled strategies for dimension , discretizing states and measurements to accuracy , and evaluate the winning probability of each. These values converge to 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 at some finite .
Step 3. Accept the moment some strategy scores above . If the value is , so a finite crosses and the search halts and accepts; if no strategy ever exceeds , 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 , 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
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 , receives bits , and the provers win iff .
Step 1. Over deterministic strategies , the win condition can be satisfied for at most of the 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 . 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 . Alice measures observables , ; Bob measures , , each with eigenvalues . Why: mapping outcome bits to signs turns the parity win condition into a correlation, and these particular axes sit at the angles that maximize it.
Step 3. Form the Bell operator . Since , one finds , and each commutator has norm at most , so and . The chosen strategy attains , Tsirelson's bound. Why: the commutator term is the purely quantum piece; classically the observables commute and the bound collapses back to , the classical Bell limit.
Step 4. Convert the Bell value to a winning probability with . At the Tsirelson value , beating by . Why: the coefficient is , not — the four question pairs each carry weight and the correlation-to-probability map contributes a further factor , so the probability stays safely below .
Step 5. Rigidity: any strategy reaching must, up to a local isometry, use the maximally entangled pair and anticommuting observables 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 is what gives , and the numerical check confirms the winning probability.*
Go deeper · Derivation C · 2 minFrom compression and self-reference to undecidability
Here we assemble the hard inclusion by combining gap-preserving compression with Kleene's recursion theorem to manufacture, for any Turing machine , a finite nonlocal game whose entangled value is exactly when halts and at most 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 terminates.
Step 1. Establish the compression primitive: a polynomial-time map sending a verifier with runtime to with , such that has the same gap behaviour as . Internally forces the provers to share an exponentially larger entangled state and to answer questions about a low-degree encoding of '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 , a verifier can accept its own compressed description as input. Define a verifier that, given code , computes 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 satisfying . Each query to 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 into the base case so the infinite unfolding attains value precisely when 's computation halts, and is capped at 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 ; since it is -complete, every language reduces likewise, giving . With Derivation A, 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 against its neighbours shows exactly which resource does the work — the second prover, the entanglement, and the infinite dimension are each load-bearing.
| Case | Result | Meaning |
|---|---|---|
| No entanglement (classical MIP) | Babai–Fortnow–Lund: two non-communicating classical provers with a poly-time verifier decide nondeterministic exponential time. Entanglement strictly increases power, since . | |
| Single prover, quantum messages | 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 model | With commuting-operator strategies the value is semidecidable from above via the NPA hierarchy. Equality with would force decidability — impossible — so the two models differ. | |
| Halting instance (completeness) | halts | Honest provers with a growing, possibly infinite-dimensional entangled state win with probability tending to ; if never halts the value is capped at . |
| Provers and rounds | 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 demand equal to respectively. Any fixed pair of answer functions satisfies at most three of these — the AND being true only for is the obstruction — so the best classical winning probability is .
Step 2. Bell value of the quantum strategy. With the Bell pair and the observables , each of the four correlators equals , and the signed sum gives , saturating Tsirelson's bound .
Step 3. Winning probability. Apply . Numerically , so , and equivalently .
Step 4. The advantage. The entangled provers beat the classical ceiling by — 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 grid with entries in so that every row multiplies to and every column multiplies to . Multiplying all nine entries row-wise gives but column-wise gives — 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 of the row–column pairs, so .
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 along rows and 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: .
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 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
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 , the ceiling now universally called Tsirelson's bound; it is the value Derivation B saturates and the reason the quantum winning probability lands at rather than . 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 on 13 January 2020, they answered it in the negative: . 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.
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 , Tsirelson bound , and winning probability ; magic-square values, classical and quantum ; the chain ; and , , and the compression-plus-recursion structure of . The winning-probability coefficient is , so no value exceeds .
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 halts there exists a perfect entangled strategy for , and when runs forever every strategy is capped at . The undecidability sits in the abstract value , 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 . CHSH and the magic square are the two smallest interesting examples, and every protocol is ultimately a family of such games.
Which direction of the theorem is the hard one?
The inclusion 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 . 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 II von Neumann factor embeds, in trace, into an ultrapower of the hyperfinite II 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 equals the commuting-operator set . 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 makes deciding it as hard as halting — undecidable. Hence , and Connes' conjecture is false.
What is compression really doing?
Compression is a transformation on verifiers. Given a verifier whose game takes time to check, it produces a new verifier whose description is only 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: makes them share an exponentially larger entangled state and answer questions about an encoded transcript of 's computation, while rigidity tests (Pauli braiding, introspection) prevent them from lying about that state. The payoff is self-reference: because 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 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.