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
The expanded state
2.5
Naimark dilation against a fixed state
2.6
The commutation analysis
2.7
Attaching a projection, and the pasting lemma
2.8
Generalized Pauli observables
2.9
Computability conventions
2.10
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
4.4
Deciding a cost budget, and semideciders on encoded values
5
Parallel repetition
▶
5.1
Direct parallel repetition
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
Semidecision from both sides
8.3
Upper semidecision through a Positivstellensatz
8.4
Correlation sets and the conditional separation
8.5
Failure of Tsirelson’s problem
8.6
Separation of quantum and commuting values
8.7
Refutation of Connes’ Embedding Problem
8.8
Failure of Kirchberg’s QWEP conjecture
8.9
The commuting-operator class
8.10
Further directions
8.11
Provenance of this chapter
9
The Aldous–Lyons track: \(\mathrm{TMIP}^* = \mathrm{RE}\)
▶
9.1
Tailored games and permutation strategies
9.2
Tailored normal form verifiers
9.3
The target
9.4
Compression and its three stages
9.5
Tabulation, the search program and the reduction
9.6
The polynomial-time class
9.7
Question reduction: the honest strategy as a permutation strategy
9.8
Answer reduction: linear systems over \(\mathbb {F}_2\)
9.9
Answer reduction: succinct descriptions through three windows
9.10
Answer reduction: the output indicator
9.11
Answer reduction: the PCP and its soundness
9.12
Answer reduction: the completeness of the PCP
9.13
Answer reduction: the answer-reduced game
9.14
Completeness of the answer-reduced game
9.15
Soundness of the answer-reduced game
9.16
The output verifier’s programs
9.17
Answer reduction: the parameters and the contract
10
The Aldous–Lyons conjecture: subgroup tests
▶
10.1
Subgroup tests and the conjecture
10.2
The test associated with a tailored game
10.3
The sofic value is not approximable
10.4
The measure side: Main Theorem I
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
The expanded state
2.5
Naimark dilation against a fixed state
2.6
The commutation analysis
2.7
Attaching a projection, and the pasting lemma
2.8
Generalized Pauli observables
2.9
Computability conventions
2.10
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
4.4
Deciding a cost budget, and semideciders on encoded values
5
Parallel repetition
5.1
Direct parallel repetition
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
Semidecision from both sides
8.3
Upper semidecision through a Positivstellensatz
8.4
Correlation sets and the conditional separation
8.5
Failure of Tsirelson’s problem
8.6
Separation of quantum and commuting values
8.7
Refutation of Connes’ Embedding Problem
8.8
Failure of Kirchberg’s QWEP conjecture
8.9
The commuting-operator class
8.10
Further directions
8.11
Provenance of this chapter
9
The Aldous–Lyons track: \(\mathrm{TMIP}^* = \mathrm{RE}\)
9.1
Tailored games and permutation strategies
9.2
Tailored normal form verifiers
9.3
The target
9.4
Compression and its three stages
9.5
Tabulation, the search program and the reduction
9.6
The polynomial-time class
9.7
Question reduction: the honest strategy as a permutation strategy
9.8
Answer reduction: linear systems over \(\mathbb {F}_2\)
9.9
Answer reduction: succinct descriptions through three windows
9.10
Answer reduction: the output indicator
9.11
Answer reduction: the PCP and its soundness
9.12
Answer reduction: the completeness of the PCP
9.13
Answer reduction: the answer-reduced game
9.14
Completeness of the answer-reduced game
9.15
Soundness of the answer-reduced game
9.16
The output verifier’s programs
9.17
Answer reduction: the parameters and the contract
10
The Aldous–Lyons conjecture: subgroup tests
10.1
Subgroup tests and the conjecture
10.2
The test associated with a tailored game
10.3
The sofic value is not approximable
10.4
The measure side: Main Theorem I