1 Introduction

This blueprint organizes a Lean formalization of the theorem \(\mathrm{MIP}^*= \mathrm{RE}\) of Ji, Natarajan, Vidick, Wright and Yuen  [ 1 ] . The main result is that there is a computable map from Turing machines to nonlocal games that sends halting machines to games of (quantum) value \(1\) and non-halting machines to games of value at most \(\frac12\); in particular, approximating the quantum value of a nonlocal game is an uncomputable problem. Through the work of Fritz  [ 18 ] , Junge et al.  [ 17 ] and Ozawa  [ 19 ] , this refutes Tsirelson’s problem and Connes’ Embedding Problem.

The main theorem is stated in the self-contained (other than importing Mathlib) file HaltingGameValue.lean. Every definition it contains (POVMs, synchronous games, game descriptions) is elementary linear algebra and computability.

Status (September 2026). The main theorem, and with it \(\mathrm{MIP}^*= \mathrm{RE}\) and the uncomputability of the game value, are proved in Lean with no hypothesis: HaltingGameValue.halting_reduces_to_gameValue (MIPRE/MainTheorem.lean) proves the statement of HaltingGameValue.lean, and #print axioms shows only propext, Classical.choice and Quot.sound. The proof is the compression pipeline, Theorem 6.197, with its three stages supplied: introspection for seven-level inputs, answer reduction over the classical PCP decider, and parallel repetition (Theorem 6.198). The goals of this project are to (a) complete a formalization of this theorem and (b) do it in such a way that the required effort benefits the community down-the-line, e.g. by making the proof modular, stating and proving as many facts as possible in a manner that is reusable, etc. Finally, (c) we expect multiple simplifications and clarifications to the proof to accompany the effort.

This initial blueprint is a coarse sketch. It maps out the main steps of the proof, in the attempt to modularize it and provide a diversity of entrypoints to the formalization effort. The most important definitions are complete, but most theorems appear only in “headline” form, with the decomposition into formalizable lemmas left as a project task.

1.1 Overview of the proof

The inclusion \(\mathrm{MIP}^*\subseteq \mathrm{RE}\) is elementary: the value of a game can be approximated from below by enumerating tensor-product strategies (Section 3.11). The substance is \(\mathrm{RE}\subseteq \mathrm{MIP}^*\), which is proved by a reduction from the halting problem. The central ingredient in the proof is a gap-preserving compression procedure for “normal form” verifiers (Section 6.6): a polynomial-time transformation that maps a verifier \(\mathsf{V}\) to a verifier \(\mathsf{V}^{\textsc{Compr}}\) which, at index \(n\), simulates the exponentially larger game \(\mathsf{V}_{2^n}\), preserving the value-\(1\) property and the property of having value at most \(\frac12\). Given compression, an abstract fixed-point argument (Lin’s compressibility criterion, Section 4.3, applied via Kleene’s recursion theorem) produces the halting reduction.

Compression itself is assembled from three transformations, each described in Section 6: question reduction by introspection (the players sample their own questions, certified by a Pauli-basis self-test built on the quantum low individual degree test), answer reduction by PCP composition (the players prove, via a probabilistically checkable proof, that their answers would have been accepted), and gap amplification by parallel repetition (anchored in  [ 1 ] , direct here). Each of these steps has one central ingredient that can be formalized in an independent manner: the low individual degree test, the PCP theorem (in a specific form), and a parallel repetition theorem (Section 5; the direct, value-form theorems are formalized).

1.2 Entry points

Contributors with different scientific backgrounds can enter the project in different places, largely independently.

Quantum information. The foundations chapter (Section 2) and the required results on self-testing: the Magic Square game (Section 3.4), the Gowers–Hatami theorem (Section 3.1), the orthonormalization lemma (Section 3.3), and the low individual degree test (Section 3.6). These are self-contained statements about states and measurements, formalizable without any complexity theory.

Complexity and computability theory. The computability toolkit (Section 4.2), the abstract recursive compression lemma (Section 4.3), succinct descriptions and the Cook–Levin machinery feeding answer reduction (Section 3.8). These are classical statements with no quantum content, and several partially exist in Mathlib.

Operator algebras. The synchronous framework of Section 2, the bridge between synchronous and tensor-product values (Section 3.2), and the downstream consequences (Section 8), which connect the main theorem to Tsirelson’s problem and Connes’ Embedding Problem.

In addition, contributors can participate at different levels. Contributors with a high degree of Lean expertise may want to focus on the foundations and concentrate on those elements of the proof that are of broader interest and may later be upstreamed to Mathlib, Physlib, CSLib, etc. For example, the Gowers Hatami theorem, general facts about Turing machines and computability, the PCP theorem, formalization of quantum games and quantum game values, etc.

1.3 Departures from the paper

The formalization is not intended to follow  [ 1 ] line by line. Since the initial publication of the paper a number of simplifications have appeared in the literature. In particular, we plan to incorporate the following.

Bipartite soundness and synchronous completeness.

The compression pipeline keeps the paper’s bipartite tensor-product value \(\mathrm{val}^*\) throughout (Remark 6.8). Synchronous strategies and the value \(\mathrm{val}^{s}\) provide the vocabulary for the final Lean statement and the doubled-game completeness witnesses; they do not replace arbitrary bipartite strategies in the inner soundness proofs. Consequently the pipeline does not invoke almost-synchronous transport to recover a gap from \(\mathrm{val}^{s}\). That transport remains part of the paper’s tensor-code route, with its explicit marginal hypotheses, and is separate from the alternative formalized classical low-degree theorem. A bridge between the paper’s and the formalization’s PCC conventions must preserve the stated completeness properties, not merely game value (Definition 2.7).

Projective strategies via orthonormalization.

The orthonormalization lemma (Section 3.3) replaces almost-projective POVMs by nearby projective measurements on the same space when its quantitative hypothesis has been established. This is distinct from Naimark dilation, which enlarges the space and is available where a bipartite argument permits it. Each soundness lemma must state the strategy class it accepts and pay for any rounding step; projectivity is not a blanket assumption on arbitrary near-optimal strategies.

Computable rather than polynomial-time, where possible.

The final undecidability statement only needs the halting reduction to be computable; polynomial-time bounds matter only inside the compression recursion, where the runtime of \(\mathsf{Compress}\) must be smaller than the succinctness it exploits (see the discussion in  [ 11 ] ). The blueprint keeps time bounds where they are load-bearing (normal form verifiers, compression) and drops them everywhere else. In particular the main theorem (Section 7) is stated with a computable reduction.

Abstract compression, in value form.

The fixed-point argument that turns compression into a halting reduction is stated once, abstractly, as Lin’s compressibility criterion  [ 13 ] (Section 4.3): a compression procedure preserving “perfect PCC strategy” and “quantum value at most \(\frac12\)”, together with the semidecidability of “quantum value above \(\frac12\)”, yields the reduction. This isolates all uses of Kleene’s recursion theorem in one quantum-free lemma, and it removes the entanglement bookkeeping of  [ 1 ] from the pipeline: no transformation needs an entanglement clause, and gap amplification uses direct rather than anchored parallel repetition, for which complete formalizations exist (Section 5.1). The recursive compression lemma of Marks–Nezhadi–Yuen  [ 11 ] , instantiated with \(f = \) entanglement requirement, is retained as the entanglement-form alternative (Remark 6.207).

Other candidate simplifications (to be decided).

Using de la Salle’s quantitative improvements to stability (Gowers–Hatami) where they shorten proofs; other simplifications that are present in the follow-up proof of \(\mathrm{MIP}^{\mathrm{co}}=\mathrm{coRE}\)  [ 12 , 13 ] .

1.4 Conventions

Every definition and theorem carries a \label, and \uses annotations record the dependency graph rendered on the project web page. Lean declaration names (\lean tags) identify the actual declarations; a statement-level \leanok records a formalized statement, and a proof-level mark records a guarded proof. An implication from a transformation structure remains conditional until that structure is supplied. Sections 3–5 distinguish formalized results, source theorems and open adapters individually; their common placement does not make them all imports or all proved. Numerical constants in headline statements (error exponents) are copied from  [ 1 ] and should be treated as provisional until the corresponding section is worked out in detail. The level budget is an exception: it is derived here, and the \(7\) levels of Theorem 6.197 differ from the paper’s \(9\) precisely because direct repetition adds no anchoring level.