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.
- 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?
- 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?