1
Introduction
▶
1.1
Overview of the proof
1.2
Entry points
1.3
Departures from the paper
1.4
Conventions
2
Foundations
▶
2.1
Games, strategies, and values
2.2
Linear constraint system games
2.3
Distance measures
2.4
Computability conventions
2.5
Normal form verifiers
3
Background results
▶
3.1
The Gowers–Hatami theorem
3.2
Almost-synchronous correlations
3.3
The orthonormalization lemma
3.4
Magic Square rigidity
3.5
The classical low individual degree test
3.6
The quantum low individual degree test
3.7
Undecidability of the halting problem
3.8
Cook–Levin and succinct satisfiability
3.9
Self-dual normal bases
3.10
The Schwartz–Zippel lemma
3.11
Approximating the value from below (\(\mathrm{MIP}^*\subseteq \mathrm{RE}\))
4
Computability
▶
4.1
The machine model
4.2
Efficient computability toolkit
4.3
The abstract compression lemmas
5
Parallel repetition
▶
5.1
Direct parallel repetition
5.2
Background results
5.3
The anchoring transformation and the theorem
5.4
Decomposition of the proof
6
Structure of the proof
▶
6.1
Conditionally linear functions and samplers
6.2
Question reduction: introspection
6.3
Oracularization
6.4
Answer reduction
6.5
Gap amplification: parallel repetition
6.6
The compression theorem
6.7
The halting reduction
7
The main theorem
8
Downstream results
▶
8.1
Uncomputability of the value
8.2
Separation of quantum and commuting values
8.3
Failure of Tsirelson’s problem
8.4
Refutation of Connes’ Embedding Problem
8.5
Failure of Kirchberg’s QWEP conjecture
8.6
Further directions
Dependency graph
MIP\(^*\) = RE: a Lean blueprint
The MIP\(^*\) = RE formalization project
1
Introduction
1.1
Overview of the proof
1.2
Entry points
1.3
Departures from the paper
1.4
Conventions
2
Foundations
2.1
Games, strategies, and values
2.2
Linear constraint system games
2.3
Distance measures
2.4
Computability conventions
2.5
Normal form verifiers
3
Background results
3.1
The Gowers–Hatami theorem
3.2
Almost-synchronous correlations
3.3
The orthonormalization lemma
3.4
Magic Square rigidity
3.5
The classical low individual degree test
3.6
The quantum low individual degree test
3.7
Undecidability of the halting problem
3.8
Cook–Levin and succinct satisfiability
3.9
Self-dual normal bases
3.10
The Schwartz–Zippel lemma
3.11
Approximating the value from below (\(\mathrm{MIP}^*\subseteq \mathrm{RE}\))
4
Computability
4.1
The machine model
4.2
Efficient computability toolkit
4.3
The abstract compression lemmas
5
Parallel repetition
5.1
Direct parallel repetition
5.2
Background results
5.3
The anchoring transformation and the theorem
5.4
Decomposition of the proof
6
Structure of the proof
6.1
Conditionally linear functions and samplers
6.2
Question reduction: introspection
6.3
Oracularization
6.4
Answer reduction
6.5
Gap amplification: parallel repetition
6.6
The compression theorem
6.7
The halting reduction
7
The main theorem
8
Downstream results
8.1
Uncomputability of the value
8.2
Separation of quantum and commuting values
8.3
Failure of Tsirelson’s problem
8.4
Refutation of Connes’ Embedding Problem
8.5
Failure of Kirchberg’s QWEP conjecture
8.6
Further directions