[FOM] Machine-checkable proofs: NP, or worse?

[Timothy Y. Chow]

On Sun, 24 Jun 2007, joeshipman at aol.com wrote:
> Another way we could achieve moral certainty is with an interactive proof.

Yes, it occurred to me that the IP = PSPACE theorem might be relevant, but 
as you point out, this takes us in a different direction.

> The other possibility is that I am misunderstanding your use of the word 
> "feasible" to mean polynomial time, whereas you are in fact assuming 
> that even when a computer runs in a "feasible time", the trace of the 
> computation may be too large to write down in a "feasible amount of 
> space".

Indeed, that is exactly my point, as you'll see if you re-read my original 
article carefully.  In practice, searching certain trees may take 
"exponential time" but be feasible, yet the trace of the computation, 
which takes "exponential space," may not be feasible to write down.

Tim