Technical Perspective: On Proofs, Entanglement, and Games

What is a proof? Philosophers and mathematicians have pondered this question for centuries. Theoretical computer science offers a rigorous handle on this deep question. One can think of a proof as a two-player game: an all-powerful though un-trusted prover who provides a proof of the statement, and a computationally weak verifier who needs only to verify it. In fact, NP problems can be presented exactly in this verifier-prover language. Viewing proofs as games turned out to be remarkably fruitful. For example, interactive proofs were invented, resembling Socratic dialogues; these are games in which the prover and verifier exchange (possibly randomized) messages. And, why just one prover? In multi-prover interactive proofs (MIP) several non-communicating provers are involved. This gave birth to beautiful concepts such as zero knowledge and probabilistically checkable proofs (PCPs) with immense impact not only theoretically but also in practice, for example, in digital currency.

The following paper studies quantum interactive proofs. Here the provers are allowed to share an entangled quantum state; this resembles sharing a random bit string, except quantum states have those funny, stronger-than-classical correlations; a prototypical example is the Einstein-Podolsky-Rosen (EPR) state, which was said by Einstein to allow "spooky action at a distance." Can quantum correlations be used to prove stronger statements?

The class of problems solvable by multi-prover quantum interactive proofs is denoted MIP^*. Its computational power had been open for over 15 years. In the following tour-deforce paper, the culmination of a remarkable line of works, the question is finally settled. While it was believed at first that MIP^* equals its classical counterpart MIP, it turns out that MIP^* contains the halting problem! The result not only resolved the stubborn MIP^* question, but at the same time solved several major decades-old open problems in mathematics. What ideas make this result so far reaching?

Best to start our journey into the MIP^* rabbit hole with the landmark 1991 result, showing that MIP equals NEXP, a scaled-up version of NP where the verifier needs to check exponentially long proofs. In MIP, the verifier only exchanges polynomially many bits with the provers—How can it verify the proof without fully reading it? The key tool is low degree tests, which leverage robustness of low-degree polynomials to allow the verifier to check, using little communication, that both provers hold consistent such polynomials. In 2011, it was shown that the protocol is secure even against entangled provers. MIP^* is thus at least as powerful as its classical counterpart.

But the point of the current paper is that MIP^* is provably much larger than MIP. How can entanglement help? Insight can be drawn from a 2019 paper, which showed for the first time that MIP^* is strictly larger than MIP. The paper proved that MIP^* contains the class of problems requiring doubly exponential long proofs (NEEXP). How can the verifier check such a proof, when even specifying a single location in the proof requires exponentially many bits?

Entanglement comes to the rescue. More precisely, a remarkable property of entangled states called self-testing. In 1964, Bell had devised a game in which two players who share an EPR state can win with a strictly larger probability than classically possible. Uniqueness of the players' optimal strategy implies that achieving maximal success probability serves as a certificate that their state and measurements are the unique optimal ones. This is a remarkable form of rigidity of quantum mechanics. It is as if the verifier gets to peek into the secret quantum labs of the provers! Moreover, a quantum version of low-degree tests enables self-tests that verify exponentially long entangled states, using only polynomial communication. Now comes a mind-boggling idea: though the verifier's messages are too short to specify its exponentially long questions about the doubly exponentially long proof, it can use quantum self-testing to efficiently force the provers to share an exponentially large, entangled state and then to correctly sample their questions themselves.

This result is just the start of the story; going all the way to the halting problem requires modifying the "compression-by-entanglement" idea so it can be applied recursively. A plethora of new hurdles arise, whose solution is the tour de force in this paper.

The exciting applications include constructing infinite algebras that cannot be approximated in any finite dimension and separating quantum correlations models previously conjectured to be equal. Self-testing is connected to group stability, which raises hope for progress on major problems in group theory.

How to explain the strong impact this theoretical computer science result has on pure mathematics? PCPs and other powerful computational complexity concepts are applied here, but perhaps another aspect is the role protocols play in the result. These sequences of individual steps that depend on time, constitute an intuitive way to think about highly complex mathematical objects, an approach that seems to offer a fresh look at physics and mathematical problems.