MIP* = RE has the startling consequence that, in the entangled provers model, there is an interactive proof for the Halting problem. In other words, for all Turing machines M that halt, two separated but quantum entangled provers can convince a classical verifier that M eventually terminates --- and furthermore the complexity of the verifier does not depend on the running time of M!

What does it mean to have an interactive proof for an undecidable problem, and how does quantum entanglement enable this mind-boggling leap in complexity for multiprover interactive proofs? In this talk, I will try to shed light on these questions by highlighting the central role of proofs in MIP* = RE: at its core, the MIP* protocol for the Halting problem recursively combines proofs of both classical and quantum properties. Time permitting, I will also discuss how the techniques in MIP* = RE point to a broader set of questions about "noncommutative property testing."

Based on joint work with Zhengfeng Ji, Anand Natarajan, Thomas Vidick, and John Wright.