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

[Mitch Harris]

On 6/14/07, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> Tacitly, many people think of the problem of finding feasible proofs of
> mathematical theorems as an NP problem.  That is, it might be hard to find
> a proof, but once the proof is found, it is in principle straightforward
> to write it down and check its correctness.

Of course only as an analogy about difficulty. Most mathematical
problems can't be forced specifically into the NP equivalent format of
propositional formula (that statement can be taken formally or
informally).

>From a different perspective, very few classes in the
complexity/decidability hierarchy can be stated in terms of a
distinction between decision time and verification time (any class on
a non-deterministic machine has an interpretation involving a suitable
witness and deterministic version of the machine, but there are far
more machine properties defining complexity classes than plain old
non-determinism). For the other classes, it is not so clear how to
distinguish proof finding (calculation) and proof verification
(calculation check).

> I believe that this is also
> one of the tacit assumptions behind the various projects that aim to
> encode all the proofs in the mathematics textbooks and journals in
> machine-checkable form.

Sure, but there we have the proof in hand to be verified in the
language and primitives of our choice, the verification (usually)
intended to be followed by a human, and presumably an appropriate
proof verifier, in linear time; only recently has it been accepted
practice to have a proof step that requests the reader, say, to solve
some large system of equations otherwise not doable by hand.

...

> Here I want to raise another issue which I suspect has not received as
> much attention.  Namely, I want to question whether NP is really the
> correct complexity class to have in mind here.

Only as an analogy.

> What made me think about
> this was Jonathan Schaeffer's announcement that the initial position of
> checkers may be solved within a year.
>
> IF he does make this announcement, should we believe him? From the point
> of view of machine-checkable proofs, we should really demand a
> machine-checkable certificate that a standard proof verifier (knowing
> nothing special about checkers) can validate.  The catch, of course, is
> that for a game like checkers, such proofs might be exponentially long.

In some sense, all we care about is an O(1) size proof for the
constant '8x8 checkers'.

> The certificate for the initial position in checkers is probably not all
> that big, but it does raise the question of whether the NP way of thinking
> is really correct.  One can certainly imagine mathematical theorems that
> have feasible proofs in the sense that the "polynomial space" and the
> "exponential time" required to verify their correctness are both within
> the realm of feasibility, but where the "exponential space" required to
> store the certificate is not feasible.
>
> One might respond to this objection by dismissing checkers as an anomalous
> instance, and that "most mathematical proofs aren't like that."  I would
> personally be rather wary of such a generalization.  Who knows what the
> future may bring?
>
> What I would like to see is either
>
> 1. an argument that this is not really a problem, for example because any
>    such scenario could be handled by a "universal" verifier that can
>    simulate an arbitrarily complex calculation while maintaining a fixed
>    upper bound on the amount of code that is required to be bug-free; or
>
> 2. an argument that, subject to some complexity-theoretic assumptions,
>    this really *is* a potential problem and there's not much we can do
>    about it.
>
> Does anyone see how to make either one of these arguments?

Let me try for supporting #2. Consider any EXP-complete problem (e.g.
prove that two regular expressions with a squaring operator are
equivalent). The complexity class just says that the proof of
equivalence could take exponential time. But there's no guarantee that
for some pair a proof might take less time).

Since 'winnability in nxn checkers' is in PSPACE', the
proof/calculation for 8x8 might be bad. And even if some one claims to
have one, it may take a long time, as far as we can guess now, even
exponential in the size of the proof to check it.

Or we might get lucky and the specific proof might be efficiently
checkable. But I don't think you can get a guarantee on some
'universal' verifier

-- 
Mitch Harris