Suppose a person comes to me, claiming some fact is true. How can I check whether they're telling the truth? I could ask them a series of questions, carefully chosen to expose any lie. Such a procedure is called an "Interactive Proof" (IP). It turns out, there is an upper limit to how 'complicated' the statement being proved can be, before I, a 'simple' verifier, can't possibly tell the difference between a true claim and a false claim. The limit is called PSPACE. Note that in order for the prover to prove such 'complicated' claims, the prover must be very 'complicated' itself - at least as complicated as the statements being proved.
How can we take things farther? Suppose that instead two people come to me, claiming some fact is true. Then, those two people are separated - they are not allowed to communicate. Then, I ask them both questions, again trying to ferret out lies. This procedure is called a "Multi-prover Interactive Proof" (MIP). Again, there is a limit to how 'complicated' the statement being proved can be before I, a 'simple' verifier, can't possibly tell the difference between a true claim and a false claim. This time, the limit is NEXP - thought to be significantly more 'complicated' than PSPACE. Again, note that the prover must be capable of very 'complicated' computations to reach this point, but the only limit based on my ability to verify the proofs is NEXP.
Now for the new result:
How can we take things further? Suppose that again two people come to me, claiming a fact is true. This time, before the two people are separated, they divvy up some entagled quantum states. Then they're separated, and not allowed to communicate. Then, I ask them both questions, again trying to ferret out lies. This procedure is called a "Quantum Multi-prover Interactive Proof" (MIP*). This time, things are different: There is (basically) no limit on how 'complicated' the statement being proved can be before I, a 'simple' verifier, would not be able to distinguish true and false claims. (Basically) The only limit on the ability of the provers to prove things to me is their ability to discover the claims, not my ability to verify those proofs. That's roughly what saying that the limit is RE is saying - there's no limit.
I don't understand, how this is possible. Is it assumed that every lie is necessarily a Bernoulli trial with a known probability? Because if not, what prevents a single oracle from telling consistently false story, taking into account all lies he told you before?
I'm pretty sure there must be some additional constraints, otherwise I don't see how you could possibly detect a lie that you cannot verify yourself with a single oracle.
Verifier: Here are two graphs, A and B. Are they isomorphic? (Same except for relabeling vertices)
Prover: No, they're different.
Verifier: Here's one of the graphs, with the vertices relabeled uniformly randomly. Which one was it?
Prover: It was A.
(Repeat 100 times)
Verifier: Ok, you got them all right. I believe you.
Here, we've forced the prover into a situation where if it's lying, and graphs A and B are in fact isomorphic, it can't know which graph we started with, before permuting. As a result, it can only guess which graph we started with and hope to get lucky, and we'll catch it with very high probability.
In contrast, if the verifier was telling the truth, it could figure out which graph we started with, and always answer correctly.
Here it is impossible for the prover to make its lie, "the graphs are not isomorphic" consistent with its later inability to tell them apart, after random permutation.
This kind of 'catching in a lie' is how interactive proofs typically work.
You cannot ask a question that would require a non-polynomial computation to provide an answer and expect it to be answered correctly.
Most importantly, recursive enumerable already means semidecidable. (Because it consists of primitive recursive functions, which are bounded.) Which means by Godel's theorems it is stronger than Peano arithmetics. (See Tennenbaum's theorem, Presburger arithmetics is fine.)
So how would the new finding override this? Or is it just <wiggles fingers> quantum magic that's running the proof in parallel in infinite entangled multiverses or something?
This does not give provers any new tricks for solving hard problems. This puts a ceiling on the power of this sort of prover-and-verifier proof and what it can show. There are problems harder than Halting (that is, that are hard even with oracles for Halting ) and MIP* doesn't contain them.
My question remains, how does this tie back to the proof? Is there a path to building such an oracle now?
Reversible computing in general seems weird when it comes to time.
Also note that this result still ultimately involves oracles with unlimited computational power (it does not construct these oracles). The interesting part is that these oracles are potentially malicious and can lie and it is the verifier's job to come up with a strategy to play an interactive game with these oracles to tease out the real answer (with a high probability of correctness).
I don't think this is correct. I believe that it only makes the Halting Problem verifiable to a simple verifier dealing with two entangled verifiers. So a verifier typically has to rely on an oracle to solve the Halting Problem, but this new proof eliminates the need for that trust by a verification procedure using two entangled oracles.
Imagine that you stumble on two infinitely powerful computers that share a bunch of entangled quantum state. Further, let's say you know how to write software for them but you need a way to check that the answers are correct. And you want to know with near certainty that your programs ran correctly, even if one of the infinitely powerful computers is evil and will use its entire intellect to convince you of something that's untrue.
Aside: this means that cryptography doesn't work---you can't use the discrete log assumption to solve this problem, you can't use collision resistant hashing, etc.
Ok, so this paper shows that, if you can figure out how to program those computers to solve the halting problem, you can then create an error detection protocol (see below) that you can check on a laptop computer and that almost perfectly (like, except with exponentially small probability) detects errors in your halting detector's execution.
You can use your laptop to ensure that your infinitely powerful, possibly evil lunatic twin Hal2^9000s aren't lying to you. Or, as BFLS91 says, "controlling a herd of supercomputers from [your iPad]" ;)
(Your error detecting protocol checker must be verified, but it's not too complicated an algorithm and we basically know how to write certified computer software for our laptops.)
(Oh, and also note that you need a perfect random number generator, and your laptop has to communicate with the supercomputers while they're executing.)
[edit for slightly more precision]
But amazing result.
Just imagine, you're about to get a proof that some program halts and just before you verify it you are eaten by a grue.
The the linked Scott Aaronson blog and associated video are fascinating.
From what i read it has something to do with refuting the Connes embedding conjecture, but i dont actually know what that is