> These are about my views on the subject, although yours are better informed
> than mine. My underlying question was, why do you suppose human
> mathematicians tend (in my observations) to trust human proofs more than
> machine proofs, especially when machines are so devastatingly precise in
> some ways, a good deal of the time, barring omitted commas (in Fortran --
> remember that one in the space program),electical surges or failurs, memory
> problems (both computer and programmer), stray cosmic rays, etc.?
My experience seems to be different from yours. I don't find any distrust
of computer proofs in general. When the computer part is just routine
calculations, now matter how long they take, I don't hear any complaints.
When the program is long and complicated, there's a natural worry that only
one or two people will have gone through it, and so a perfectly rational
feeling that it's unsafe. I think this is perfectly reasonable, and should
not be regarded as a distrust of the involvement of computers per se.
> Underlying this question, I think, are questions about what constitutes a
> proof, and such matters as Hilbert's program, Goedel's theorems and all
> that arise.
I don't. I think it's just a question of assessing reliability.
> Are such questions to be considered, here at least, as getting
> away from mathematics into regions of logic and philosophy of mathematics?
I don't think they should be. There is, of course, the philosophical
question of whether the existence of a valid proof of something should
really convince us of its truth. But one shouldn't confuse this with
the question of whether a particular proof really is a valid one.
John Conway