This video explains the MIP*=RE result. We skip the proof details, just explain what the result means. Please leave comments in the comment section if something is unclear.

## Links mentioned in the video

- Proof that the halting problem can’t be solved:

https://youtu.be/92WHN-pAFCs - Using the entanglement: TBA in a few weeks. In the meantime you can watch a general primer to quantum physics: https://youtu.be/p7bzE1E5PMY
- Proof that PSPACE contains P and is contained in EXP: TBA in a few weeks.

## More comments on the video

### Part 3

We require the verifier to run in polynomial time. This has the usual definition with respect to the input’s size. This constraints the size of the proof sent by the prover, since reading 1 character costs 1 time unit.

In the video we make a distinction between honest and malicious provers. Sometimes it is defined differently: there’s only one kind of prover, and it always wants to get the verifier to accept. For w that is in L, it gets the verifier to accept by cooperating and behaving nicely. For w outside of L, it tries to get the verifier to accept by cheating.

### Part 4

MIP: In previous games, the verifier faces a single prover. Its goal was to be able to detect if the prover is lying or telling the truth. For languages inside PSPACE, the prover could do that. But languages outside PSPACE are more complicated. For these languages, the verifier can’t tell if the prover is lying or telling the truth. In MIP we help the verifier more by having two provers. The verifier can now judge if a response is a lie not just by examining the response itself, but by comparing what the two provers say. If they respond to the same question differently, one of the responses must be a lie, and the verifier can reject immediately. This added ability to detect lies helps it verify more complicated languages – all languages in the large class called NEXP.

MIP*: Here there’s something non-intuitive going on. We help the provers by giving them a quantum device, but it turns out it actually helps the verifier. The details here are complicated, adnn will be explored in future videos.