MIP^*=RE and quantum computation

Question

I recently learned about the MIP^*=RE result. I have to admit that I don't understand big parts of this paper and I am barely familiar with quantum physics. I hope my questions below make sense.

I copy the basic definitions:

IP= the class of languages with an randomized interactive proof system (that runs in polynomial time)

MIP= the class of languages with an multiprover interactive proof system

MIP^* = the class of languages with a classical polynomial-time verifier interacting with multiple quantum provers sharing entanglement.

R.E= the class of recursively enumerable languages

It was known previously that MIP=NEXP (non-deterministic exponential time) and that MIP$\subsetneq$ MIP$^*$, but it was expected that MIP$^*$ wouldn't be "very far" from MIP, definitely within the computable.

My questions:

1. Since the 1930's there have been some very clear bounds on what is computable (e.g. by a Turing machine) and what is not. Later developments, e.g. multi-tape Turing machines, non-deterministic Turing machines, Turing machines with randomization etc. can be seen as efforts to "speed-up the computations" but without changing what is computable. A function computable by a non-deterministic Turing machine is also computable by a deterministic Turing machine, although the former may run in polynomial time while the latter in exponential time. I always thought that quantum computations will bring in some sort of "exponential speed-up" but again without changing the underlying notion of computable, i.e. quantum computable = computable by a classical Turing machine.

In view of this new result is there a reason to believe otherwise? In particular, is it possible that quantum computable languages = r.e. languages?

2. Although proof assistants are in infancy right now, it is expected that in the future will play a vital role in the development of Mathematics, much like the role computers play in chess today.

Are there any consequences of the above result for the development of proof assistants? At least in theory, is there any hope that problems which are intractable by classical computers will be tractable by quantum computers?

This is more like a dream, but can quantum computations give proof assistants the boost they need to come into play in everyday Mathematics?

Answer 1

Q1: "Do you have a reference for `quantum computable = computable by a classical Turing machine' ?
A1: This follows immediately from the fact that any quantum computation can be simulated by a classical computer with exponential overhead.

Q2: Is there any result (or conjecture) that quantum machines can be (exponentially) faster than classical machines?
A2: The conjecture is that the complexity class BQP is a strict superset of BPP.

BQP is the class of decision problems solvable by a quantum computer in polynomial time, while BPP is the class of decision problems solvable by a probabilistic Turing machine in polynomial time. Both BPP and BQP are defined in terms of randomized algorithms, which are allowed to make random choices and need to reach the desired result with probability greater than 2/3.

If BQP is strictly larger than BPP, a quantum computer can provide an exponential speed-up (from non-polynomial to polynomial). This would imply that the "strong" (or "extended") Church-Turing thesis is false: a probabilistic Turing machine (which models BPP) cannot efficiently (= in polynomial time) simulate a quantum computer (which models BQP). The simulation is certainly possible if we allow for an exponentially long time, so the basic Church-Turing thesis still holds.