[FOM] Machine-checkable proofs: NP, or worse?
joeshipman at aol.com
Sun Jun 24 21:04:55 EDT 2007
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
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,
not quite, convinced me that proofs that take a feasible amount of time
check but whose certificates take an infeasible amount of space to
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.
More information about the FOM