FOM: Consensus vs Indubitability
sacook at cs.toronto.edu
Tue Sep 15 18:06:20 EDT 1998
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.
More information about the FOM