MIP* = RE

The paper in detail

In a nonlocal game a verifier sends questions \(x,y\) to two separated provers and accepts their answers \(a,b\) according to a rule \(D(x,y,a,b)\). The entangled value \(\mathrm{val}^{*}\) is the best winning probability over finite-dimensional strategies with shared entanglement. A language is in \(\mathsf{MIP}^{*}\) if instances can be mapped efficiently to games with value 1 for yes-instances and at most 1/2 for no-instances. The class could in principle be enormous, since entangled provers are unbounded, but proving lower bounds requires certifying that the provers behave as instructed, and upper bounds require computing \(\mathrm{val}^{*}\), which no one knew how to do.

The paper's question is how large \(\mathsf{MIP}^{*}\) is. The answer is that it contains the halting problem. The easy inclusion \(\mathsf{MIP}^{*}\subseteq\mathsf{RE}\) comes from searching over finite strategies: if the value is 1, some finite strategy eventually beats 1/2. The hard inclusion builds, for each Turing machine, a game that encodes its whole run.

The core is a compression theorem: a polynomial-time procedure that turns a verifier for games \(\mathcal V_N\) into one whose \(n\)-th game, of size polynomial in \(n\), has value 1 when \(\mathcal V_{2^n}\) does, value at most 1/2 when \(\mathcal V_{2^n}\) has value at most 1/2, and requires entanglement of dimension at least \(2^{2^{\Omega(n)}}\) to beat 1/2. Compression combines four ingredients: introspection (the provers sample their own long questions from shared EPR pairs, enforced by a quantum low-degree test), answer reduction (a probabilistically checkable proof replaces long answers), oracularization, and parallel repetition to restore the gap. A verifier that runs the machine for \(n\) steps and otherwise plays its own compressed version then has value 1 exactly when the machine halts.

Through the Navascués–Pironio–Acín hierarchy, which approximates the commuting-operator value from above, the undecidability rules out equality of the two correlation models, and by results of Fritz and of Junge et al. it refutes Connes' conjecture. The open problems the authors list are an explicit non-embeddable \(\mathrm{II}_1\) factor (the separating game is synchronous, which suggests a route), whether it can come from a group that is not hyperlinear, a direct way to reduce the number of provers, and the complexity of the commuting-operator class \(\mathsf{MIP}^{\mathrm{co}}\), which lies in \(\mathsf{coRE}\) and plausibly equals it.

Transferable methods

1. Self-reference turns compression into undecidability

   Compressing a known protocol once gives a bigger complexity class, but iterating it naively fails because each step changes the protocol's form. The paper instead builds a verifier that compresses itself, using a fixed-point construction, so that one compression theorem is applied infinitely often through the verifier's own definition.

   Let \(\mathcal V^{M}\) run the machine \(M\) for \(n\) steps, accept if it has halted, and otherwise play the \(n\)-th game of \(\mathsf{Compress}(\mathcal V^{M})\). If \(M\) halts at step \(T\), then \(\mathrm{val}^{*}(\mathcal V^{M}_n)=1\) for \(n\ge T\), and for \(n<T\) completeness transfers value 1 down from index \(2^n\); repeated doubling reaches \(T\), so every game has value 1.

   If \(M\) never halts, soundness keeps every value at most 1/2 or else forces more entanglement. The entanglement bound gives \[\mathscr E\bigl(\mathcal V^{M}_n,\tfrac12\bigr)\ \ge\ \max\Bigl\{\mathscr E\bigl(\mathcal V^{M}_{2^n},\tfrac12\bigr),\ 2^{2^{\Omega(n)}}\Bigr\},\] and iterating along \(n\to2^n\to2^{2^n}\to\cdots\) shows that no finite dimension suffices to beat 1/2. Since \(\mathrm{val}^{*}\) is a supremum over finite dimensions, \(\mathrm{val}^{*}(\mathcal V^{M}_n)\le\tfrac12\).

   How to reuse it

   Whenever a reduction maps a problem at scale \(N\) to a problem at scale \(\log N\) while preserving a gap, a self-referential instance that runs the reduction on itself lifts the hardness to every finite scale at once, and often to undecidability.

2. From an uncomputable value to Tsirelson's problem

   The step from complexity to operator algebras uses two approximation schemes that converge from opposite sides. If the finite-dimensional and commuting-operator values always agreed, running both would compute the value, which the halting reduction forbids.

   Enumerating rational finite-dimensional strategies gives lower bounds converging to \(\mathrm{val}^{*}(\mathfrak G)\); the semidefinite hierarchy of Navascués, Pironio and Acín gives upper bounds \(\alpha_1\ge\alpha_2\ge\cdots\) converging to the commuting-operator value \(\mathrm{val}^{\mathrm{co}}(\mathfrak G)\). If \(C_{qa}=C_{qc}\) then the two limits coincide, and running both until they differ by less than 1/4 distinguishes value 1 from value at most 1/2, contradicting undecidability.

   For an explicit separation the paper feeds the hierarchy into the construction: the game's machine halts if some \(\alpha_n<1\) for the game itself. If \(\mathrm{val}^{\mathrm{co}}<1\), the machine halts, so \(\mathrm{val}^{*}=1\le\mathrm{val}^{\mathrm{co}}\), a contradiction. Hence \(\mathrm{val}^{\mathrm{co}}=1\), the machine never halts, and \(\mathrm{val}^{*}\le\tfrac12\). Editorial note: the argument proves that a winning commuting-operator strategy exists without constructing one, which is why explicit counterexamples remain open.

   How to reuse it

   Two semi-algorithms converging from opposite sides decide any gap problem when their limits agree; an undecidability result for the gap problem therefore proves that the limits differ, which is a general route from computability to separations of convex sets.

Source: Section 2 (proof overview); Theorem 12.1; Sections 12.2–12.3. Based on the linked paper version. Derivations marked as editorial, and suggested uses in other problems, are editorial guidance rather than results of the paper.

Context & limitations

Why it matters. The theorem connects three fields through one construction: a game's value is uncomputable, so Tsirelson's problem has a negative answer, so there are type \(\mathrm{II}_1\) factors not embeddable in an ultrapower of the hyperfinite factor. After six years and a 250-page proof, two kinds of check now stand behind it: refereeing for the Annals, and a machine-checked proof whose only axioms are Lean's three standard ones. The formal development also proves the Bowen–Chapman–Vidick statement \(\mathsf{TMIP}^{*}=\mathsf{RE}\) and the resulting refutation of the Aldous–Lyons conjecture.

Limitations. The paper's separation is non-constructive in an important sense: it gives an explicit game with commuting-operator value 1 and entangled value at most 1/2, but no commuting-operator strategy that wins it, and no explicit non-embeddable factor. The games are enormous. Version 4 notes that very recent, heavily AI-assisted work gives more concrete counterexamples (non-hyperlinear groups, arXiv:2609.37761, and a linear-system game separating the two models, arXiv:2610.10248), which the authors do not survey. The formalisation departs in places from the written proof, notably by using the general parallel repetition theorem (formalised by OpenAI) and the earlier Lean proof of the low-individual-degree test by Lu, Deng and Ji. The paper states that AI was used for targeted edits and copy-editing in the final revision and that the authors used general LLM methods for the formalisation; the repository's commit history credits Claude models as co-authors on most commits.

Description based on the full arXiv HTML of v4 (16 October 2026), read 2026-11-10: Sections 1 and 2 (statement, consequences and proof overview), the statements of Theorem 12.1 and Sections 12.2–12.3, and the AI-use and Lean statements in Section 1.4. The 250-page proof was not checked line by line. The formalisation's status was read from the project README and the Palomar registry record (registered 9 October 2026, commit 7798a80), not by building it. The CHSH values quoted in the introduction were recomputed.