An Interactive Proof of God's Number? I've been learning about interactive proofs lately and I've been wondering if the whole thing was nothing more than a theoretical curiosity, or if it had any practical applications. I thought I'd start off with an example which occurred to me in the shower:

It's been making the news lately that "God's Number"=20. (God's number is the minimal number of steps needed to solve the Rubik's Cube). While this is pretty interesting,  there seems to be a little twist ... This isn't a "normal" proof in the textbook, polynomial time verifiable sense. This proof has a distinctly "brute force" flavor to it - by this I mean, the dudes at Dr Morley's lab tried with billions and billions of combinations of cubes in Google's massive supercomputers to find this neat, tight lower bound. 

Anyway, the question is: How can we be certain that Dr Morley Davidson and his team are honest? Well, right away can throw the argument from authority out of the window as it's not mathematically rigorous. The obvious alternative is to re-verify the proof, by checking the source code and running the whole thing again, which seems to be a terrible waste of computational resources, not to mention the fact that everybody who who wished to be convinced of this would need to do it on his own workstation - a very tedious and unpleasant proposition for the true skeptic. So this seems to be a kind of ontological deilema.

So what I believe is this is exactly a situation where we need an interactive proof. Google's Supercomputer could be the all powerful but deceptive Prover, and we the skeptical, if not anal members of the public are the Polynomially bounded Verifiers. If we could somehow query our "Oracle" a polynomial number of times, and be convinced of this lower bound, we could be convinced of the fact that he's right, beyond all reasonable doubt.

So it seems the Decision problem "God's Number is &lt; 20" lies in $\Pi_2^p$ or can be restated as follows (informally)

For all starting combinations $\alpha$ in the Rubik's Cube, there exists a solution which takes &lt;=20 steps, $\beta$ which solves it.

(not sure if that's correct, but $\alpha$ and $\beta$ are both small in size, given a starting configuration and a solution it's easy to verify that it does indeed solve the cube)

and the Decision problem "God's number is 20" can be restated as

God's number is &lt;20 and there exists a solution for some starting combination of the Rubik's cube which takes 20 steps.

So there's probably a IP[n] proof for this. (once again, check my workings)

My question is twofold 


Is there a actual way to do this?
What other examples of "pratical" uses of interactive proofs are there?
... it seems the Decision problem "God's Number is &lt; 20" lies in $\Pi_2^p$.


That is enough for it to have an interactive proof. In fact, Lund et al. proved that every language in polynomial hierarchy (PH) has an interactive proof by using Toda's theorem ($\rm{PH} \subseteq P^{\#P}$). They reduced $L\in \rm{PH}$ to #P-complete language PERMANENT, and provided an algebraic method which can be used to prove PERMANENT interactively. (This is highly inaccurate; please refer to the paper for more info.)

Using their techniques, Shamir proved that IP=PSPACE.

It was previously proved that all IP has zero-knowledge proofs, so:

All languages in PSPACE have zero-knowledge interactive proofs.