FOM: random aided proof

[Harvey Friedman]

Replay to Cook 6:06PM 9/15/98.

>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.

I see your objection that it does not provide an absolutely rigorous proof
(whatever that means). I see, however, a distinction. One objection (that
you make next) concerns the nature of pseudo random number generators. But
another objection might be that the Rabin procedure is such that you don't
get a rigorous proof even if, in some appropriate sense, the pseudo random
number generator is "absolutely random."

I would like to know how you view this matter. I can see that under some
definitions of "absolutely random" the Rabin procedure may well be turned
into a completely rigorous proof of primality in the normal sense of
matheamtics. Whereas under other definitions of "absolutely random" maybe
it doesn't. Another possible way of looking at this might yield the
conclusion that there is some sort of new rigorous principle here that is
as compelling as, say, the axioms of first order arithmetic or of set
theory, but quite different.

>The difficulty is that there is no practical source of random input bits which
>can be used to apply
>Rabin's algorithm.

How do you feel about the use of physical processes as random number
generators? E.g., noise from background radiation, etcetera. What do you
think of the "rigor" surrounding the idea that physical noise does not care
about whether or not your number is prime? I.e., relevant concepts of
"independence"?

>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.

There are issues connected with "why should I believe a computer?" at the
hardware and software level, and how good "independent verification" is. Do
you regard such issues as nonissues?

Finally, let me ask a question. Which is more certain to you:

a) that p is prime via a current application of Rabin's test with current
pseudo random number generators? and
b) the whole of California will not fall into the ocean on Jan. 1, 2000?

Pollock writes 2:59PM 9/16/98:

>A probabilistic test of primality using Rabin's algorithm is **no**
>evidence for the primality of a number.

I am dumbfounded by your use of the word "no." See my question to Cook above.

If you say "Rabin's algorithm
>shows m is prime to probability ..." there is no evidence to be
>checked.

But the deep foundational question is, not whether it is true, but what
does it mean?