FOM: Consensus vs Indubitability

[Stephen Cook]

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.   In practice, a pseudo random number generator is invariably
used, which is just a deterministic algorithm which starts with a (hopefully random)
initial seed.  It is far from clear that this method will generate sufficiently random
bits to make Rabin's algorithm work.   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.

On the other hand, I have no problem (at least in principle) with the use of
computers made by Appel and Haken, and later Seymour et al, in establishing
the four color theorm.

Steve Cook