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  [ 15 ] , Junge et al.  [ 14 ] and Ozawa  [ 16 ] , 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. The goal of this projects 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.

Synchronous strategies throughout.

The paper works with bipartite tensor-product strategies \((|\psi \rangle , A, B)\) on \(\mathcal{H}_\textsc{A}\otimes \mathcal{H}_\textsc{B}\). We instead take synchronous strategies — a single family of measurements \(\{ M^x_a\} \) on one space, evaluated against the tracial state — as the basic object, and define the synchronous value \(\mathrm{val}^{s}\) (Definition 2.10). This eliminates the duplication of Hilbert spaces, states, and consistency bookkeeping that pervades the paper’s soundness analyses, and it matches the main Lean statement. The cost is a single bridging step: the almost-synchronous correlations theorem (Section 3.2) shows that for synchronous games the two values agree closely enough to transport completeness and soundness. All games constructed in the proof are synchronous (or are made so by symmetrization), so this is a genuine simplification.

Projective strategies via orthonormalization.

Rather than invoking Naimark dilation to replace POVMs by projective measurements (which enlarges the space and interacts poorly with the tracial framework), we use the orthonormalization lemma (Section 3.3) to replace almost-projective POVMs by nearby projective measurements on the same space. All soundness analyses should be carried out for projective strategies from the start.

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  [ 8 ] ). 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  [ 10 ] (Section 4.3): a compression procedure preserving “perfect PCC strategy” and “value at most \(\frac12\)”, together with the semidecidability of “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  [ 8 ] , instantiated with \(f = \) entanglement requirement, is retained as the entanglement-form alternative (Remark 6.8).

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}\)  [ 9 , 10 ] .

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) are deliberately absent at this stage; they will be added as the corresponding declarations are created. Statements in Sections 3–5 are external results: the project may initially axiomatize them (each section records the literature source and comments on formalization), while statements in Section 6 are proof obligations of the project. Numerical constants in headline statements (levels, error exponents) are copied from  [ 1 ] and should be treated as provisional until the corresponding section is worked out in detail.