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

[joeshipman@aol.com]

But in all such cases, the trace of the computation could be regarded 
as a feasible size proof which takes a feasible amount of time to check.

In other words, there might be a way of representing an infeasible 
proof in a way that can be feasibly checked, but then the finite amount 
of work needed to build and prove correctness of the operating and 
proof-checking system allows one to obtain a feasible proof.

There may well be theorems with no polynomial-size proof which we can 
achieve moral certainty about by machine-checking.

One way to do this is with randomized proofs. We can come to believe 
that an input belongs to a set in the complexity class RP (random 
polynomial time) by testing a few hundred random witnesses with an 
algorithm which passes all witnesses for an input in the set but flunks 
at least half of witnesses for an input not in the set. But this is not 
the same as the situation you describe, where there is no possibility 
of "bad luck" (even though the probability of other types of error may 
dwarf the chance of picking unlucky pseudo-witnesses, the certainty 
obtained has a different epistemological status).

Another way we could achieve moral certainty is with an interactive 
proof. A being with access to resources we do not have may settle to 
our satisfaction any question involving membership in a set in PSPACE 
by an interactive proof, but here again we are inductively generalizing 
that he will be able to respond to any future queries from us as 
successfully has he has responded to our previous queries, which has a 
different epistemological status than the situation you and Weber seem 
to be discussing.

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

-- JS

-----Original Message-----
From: Timothy Y. Chow <tchow at alum.mit.edu>
To: Foundations of Mathematics <fom at cs.nyu.edu>
Sent: Sun, 24 Jun 2007 3:35 pm
Subject: Re: [FOM] Machine-checkable proofs: NP, or worse?

I've been having an email discussion with Tjark Weber, who has almost, 
but
not quite, convinced me that proofs that take a feasible amount of time 
to
check but whose certificates take an infeasible amount of space to 
write
down do not pose a problem.

________________________________________________________________________
AOL now offers free email to everyone.  Find out more about what's free 
from AOL at AOL.com.