FOM: Re: Cook on Consensus vs Indubitability

[Randy Pollack]

Cook comments (Tue, 15 Sep 1998 18:06:20 -0400)

> Joe Shipman's recent reply to Hersh gives two examples of computer
> assisted proofs.  While I agree with the thrust of Joe's argument
> (that rigorous proofs are necessary to establish consensus), I don't
> agree that the second example, establishing primality using Rabin's
> probabilistic test, provides a rigorous proof.  The difficulty is that
> there is no practical source of random input bits which can be used to
> apply Rabin's algorithm.

I agree with Cook, and want to push the point further.  It is not
"reproducibility" of rigorous proofs (like repeating a physical
experiment) that can establish consensus.  It is that proofs serve as
evidence for what they prove.  Thus if you claim "here is a proof of
X", and I care to believe X, I can check your putative proof.  If I
agree it is a proof, we have consensus.  If I don't agree, you can
demand to know what step or assumption I don't accept, and you can
explain that further, attempting to convince me.

A probabilistic test of primality using Rabin's algorithm is no
evidence for the primality of a number.  If you say "Rabin's algorithm
shows m is prime to probability ..." there is no evidence to be
checked.  You might tell me to run Rabin's test myself, but if I get a
different result there is no basis for discussion.  If you publish
your trace from running the test, why should I believe the randomness
of the "random" input.  Surely no probabilistic analysis should
convince me ex post facto.

Perhaps your trace uses a pseudo-random stream published before you
computed the trace.  This is a bit more convincing, but Cook states I
should not (yet) accept this as evidence:

> In fact, if one could prove in a general setting that some pseudo
> random number generator is sufficiently random, it would follow that
> the probabilistic complexity class BPP coincides with P, solving a
> major open problem.


>From this "proof as evidence" view, we should accept the Appel and
Haken proof as a putative proof, and we can attain belief by checking
the computation ourselves.  (That is, writing a program to test the
cases, and actually running it.)  If we disagree with Appel and Haken,
there will be a particular case that needs further study, so a path to
consensus.

However there is no sharp line to be drawn.  If a proof by computation
used, say, 6 months of supercomputer time, running complex
ultra-optimized algorithms, there is no realistic way to independently
check it, at least until faster computers become available.  What we
accept as proof, either completely formal or rigorous, depends on
actual independent checking.

-- 
Randy Pollack                      <http://www.dcs.gla.ac.uk/~pollack/>
Computing Science Dept.                         <pollack at dcs.gla.ac.uk>
University of Glasgow, G12 8QQ, SCOTLAND          Tel: +44 141 330-6055