[FOM] Machine-checkable proofs: NP, or worse?
Timothy Y. Chow
tchow at alum.mit.edu
Mon Jun 25 09:26:51 EDT 2007
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
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.
More information about the FOM