Re: [HM] Proofs and the computer
Gordon Fisher (gfisher@shentel.net)
Wed, 09 Jun 1999 14:15:19
At 01:27 PM 6/9/99 -0400, John Conway wrote:
>
>
>> > I wonder ... are some of us more apt to trust a proof gone over by
numerous
>> > humans, say as in the case of the Fermat conjecture, than to trust a
proof
>> > produced by a machine using different programs composed by different
>> > programmers? Or not?
>
> Well yes, doubtless some of us are, and some of us aren't; but the question
>of the existence of such opinions is getting quite far away from mathematics.
>
> To my mind, the only significant problem here is that of assessing the
>reliability of a proof, no matter how that proof was produced. My own
>opinion is that the major factor affecting this is the length. If a
>computer is involved, this means the length of the program; if not, the
>length of the argument.
>
> In the original 4-color proof, the computer part was very reliable,
>since it mostly consisted of reducibility checks, which used a fairly
>short and readily comprehensible program, even though its application
>to all the cases used thousands of hours of machine time. So much of
>the published comment was beside the point - it was the human part,
>not the computer part, that was unreliable. This consisted of a
>"discharge" method performed largely by hand that split the problem into
>nearly 2000 cases, and indeed many errors were found in it.
>
> For similar reasons I regard the proof of the classification problem
>for finite simple groups as unreliable, mostly because it is so long.
>(The computer involvement is very small.) The proof of Fermat's theorem
>is safer, because it has been so intensively scrutinized, but there's
>still some risk, because it's both long and subtle.
>
> John Conway
>
>
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.?
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. Are such questions to be considered, here at least, as getting
away from mathematics into regions of logic and philosophy of mathematics?
Gordon Fisher gfisher@shentel.net