# MIP*=RE theorem and its impact on logic and proof theory

In the monumental paper MIP*=RE five authors, Zhengfeng Ji, Anand Natarajan, Thomas Vidick, John Wright, and Henry Yuen, managed to show that two complexity classes: RE and MIP* do in fact coincide. My impression is that every theorem establishing an equality of two complexity classes is a major result (since it is usually notoriously difficult to equate two complexity classes) but I find this one particularly interesting, since the class of RE languages contains the (in?)famous halting problem. I would like to create some sort of a mental picture regarding what this result in fact tells us: since the halting problem is in the background I'm aware that there is a risk to become overenthusiastic and claim that this theorem would give us a tool to solve undecidable problems. I suspect that this is not the case. Still I'm wondering

What is the possible impact of this result on decidability issues and/or logic/proof theory in general?

I do not have enough expertise in complexity theory, proof theory and logic to be able to formulate my question more precisely but very roughly what I have in mind is that maybe there is some undecidable problem on which now we can shed some more light and get some evidence or reasons to postulate it as an axiom? Or maybe this result could serve as a motivation to develop some new definition of provability? Forgive me if I'm sounding like a crackpot (I'm afraid that I am)—my interest in this theorem came from operator algebras and Connes embedding cojecture which was solved in this very unexpected way.

• Since there is almost certainly no single right answer, maybe you should flag your post for moderator attention and ask that it be made CW? Sep 23, 2023 at 14:22
• I don't think the post needs to be CW. Sep 23, 2023 at 14:49
• I'm not sure exactly what you're getting at, but given the fact that quantum computers can't fundamentally do anything a Turing machine can't do, I think MIP* coinciding with computably enumerable (or r.e.) languages says more about physical unreality of the situation used to define MIP* than about anything on the logic side of thing. (See the discussion in the comments here for instance.) Sep 23, 2023 at 15:55
• Another thing to note is that while establishing equivalence of complexity classes is in general hard, establishing that a given problem is undecidable in one way or another (typically by embedding the halting problem) is often a lot easier (which isn't to say it can't be very difficult in specific cases, such as MIP* = RE). Sep 23, 2023 at 16:11
• Showing complexity classes are equal is often hard. As opposed to showing classes are different, which is usually impossible :p Sep 23, 2023 at 19:33

You wrote:

maybe there is some undecidable problem on which now we can shed some more light …

Depending on what you mean by "shed some more light," the answer is yes; the original paper already explains several novel insights into certain undecidable problems.

… and get some evidence or reasons to postulate it as an axiom?

This sounds like a confusion between the two meanings of the word "undecidable". The type of undecidability here is computational undecidability, rather than independence from some axiomatic system.

Furthermore, as mentioned in James Hanson's comment, the presence of the word "quantum" does not by itself mean that there's anything "physically meaningful" about MIP*. The MIP* set-up involves hypothetical quantum provers that can solve undecidable problems. If you're imagining that we might use the ideas in the paper to set up an experiment to physically investigate some heretofore mysterious mathematical statement, we'd first have to get our hands on some all-powerful quantum provers to interrogate. We're not going to be able to buy them on Amazon. :-)

More generally, I've explained on cstheory.SE a fundamental difficulty with any attempt to "build a hypercomputer." The short version is that even if Amazon did offer all-powerful quantum provers for sale, how could we definitively know that it wasn't false advertising?

• If two other companies independently provide a similar service, can we use the MIP*=RE result to check that all of them are advertising honestly? (And they are hyperquantum machines) Sep 24, 2023 at 13:49
• @VilleSalo The same objection that I explained on cstheory.SE applies. It really is a fundamental difficulty, rooted in the fact that human beings are finite. Sep 24, 2023 at 13:52
• I'm not sure I buy that is inconceivable to set up an experiment where you can convince yourself that someone is using an infinite process. A fanciful analogy: imagine a wall made of lead which has the property that it becomes infinitely dense, so that to see through it using an X-ray requires 1 unit of energy to go half way, 2 units to go 3/4ths, 3 units to go 7/8ths, and so on. A mystical someone claims to have an X-ray that can see with infinite power. Your assistant holds a playing card behind the wall, and the mystical someone can correctly guess the card every time. Sep 24, 2023 at 14:23
• @SamHopkins You can't have arbitrarily high density materials without forming a black hole. Sep 24, 2023 at 15:54
• @SamHopkins How do you know that the lead has the claimed property? This is engineering and not abstract mathematics. What experiment do you propose that will prove that the lead has infinite density, as opposed to "topping out" at some large density that is far beyond what we can experimentally probe? Sep 24, 2023 at 17:20

MIP* = RE does not imply that a model of quantum computation can solve undecidable problems, as you correctly intuit. Instead, it establishes the existence of (a type of) interactive proofs for the Halting problem.

In this type of interactive proof, a classical polynomial-time verifier interacts with two entangled quantum provers. You can think of the provers as making a claim of the form "Turing Machine $$M$$ halts.". If the Turing machine does halt, then there exists a strategy for the provers to convince the verifier of this fact. The catch is that the provers might have to spend a lot of time to compute this strategy (for example if $$M$$ takes a long time to halt).

If $$M$$ does not halt, then no strategy will convince the verifier to accept the claim with high probability.

The surprising thing about MIP* = RE is that the amount of work put in by the verifier to perform this verification process is independent of the running time of $$M$$, which may be infinite. The verifier's runtime only depends on the description length of $$M$$.

To reiterate, the interactive proof does not circumvent the computational difficulty/impossibility of solving the Halting problem -- it just concentrates the difficulty on the provers' side.

• If the claim is "M does not halt", does the interactive proof mechanism also give the provers a way to convince the verifier of that? Sep 30, 2023 at 16:57
• No, it does not, and necessarily so :) The reasoning for this comes from computability theory: the class $MIP^*$ is contained in $RE$, which is known not to contain $coRE$ (the class for which determining which Turing machines do not halt is complete for). Sep 30, 2023 at 20:55