🚀 go-pugleaf

In article <PHR.92Nov16003614@napa.telebit.com> phr@telebit.com (Paul Rubin) writes:
>    Mathematics would also be placed in a surprising position by P=NP.
>    P=NP implies that there is an algorithm which, given a theorem
>    expressed formally in ZF, say, and a number n, either gives a formal
>    proof of the theorem of length at most n, or shows that there is none,
>    and which would take time bounded by some polynomial in n. It wouldn't
>    *necessarily* put us all out of the math research business, but....
>
>I don't know that this is really so interesting: the kinds of things
>we write down in mathematical proofs ("by symmetry, X, and by
>induction on n, Z") often would have very large expansions in formal
>proofs.  The kind of thing a mathematician would write down as a proof
>of a theorem is less like shorthand for a formal proof than like a
>computer program which generates a formal proof.  So we're not so
>interested in the length of the formal proof as in the length of the
>shortest such program.  But recognizing whether a program P generates
>a proof of a theorem T is not in NP---it's not even undecidable
>(because we can't even tell if P ever halts).  Thus, my feeling is
>that even an NP-oracle wouldn't put mathemeticians out of business.

Traditional formal proofs are a red herring here.  Suppose as you
suggest that you indeed constitute your proof system in terms of a
program that decides according to some computational criterion whether
to accept a given proof, whether by expanding shorthand to a formally
checkable proof, ingenious dovetailing of a raft of decision methods,
or whatever.  To avoid vindicating Mattel ("math class is tough"), its
running time must be polynomial in the length of the proof (and given
the length of some proofs in the literature, shorthand or not, this had
better be well below n^5).  With this essential provision the argument
you are objecting to remains sound.
-- 
Vaughan Pratt	  		A fallacy is worth a thousand steps.