[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu, shipman@savera.com*Subject*: FOM: understanding computer proofs*From*: Stephen Cook <sacook@cs.toronto.edu>*Date*: Mon, 14 Dec 1998 10:58:29 -0500*Cc*: sacook@cs.toronto.edu*Sender*: owner-fom@math.psu.edu

I enjoyed reading Joe Shipman's December 7 illuminating discussion of the three big theorems, including his notions of the depth, width, and length of proofs. Here I want to comment on one aspect of his Dec 11 discussion of mathematical certainty, namely his suggestion that Wiles' proof of FLT is more understandable than the recent computer-aided proof of 4CT. Joe argues that the "mathematical" protion of the 4CT proof is quite well established, and many people understand it. However, the computer part "...depends on so many finite combinatorial `facts' that we still need to point to a computer output to persuade someone else that it is true". It seems to me that in general, if the use of a computer in a proof involves only straightforward, understandable algorithms, then the reliance on the computer does not degrade the understandability of the overall proof (or at least not much). To make this point, suppose that a hypothetical proof of an important result relies on verification that a certain number p is prime; say p is 8 or 10 digits long. Suppose that the verification can be carried out in an hour, using a pocket calculator for integer arithmetic, or in ten hours using long hand arithmetic with no mechanical aids. It seems to me that there is no increase in understanding gained by doing the arithmetic by hand. (In fact I wonder if there is any reason at all to do the arithmetic by hand, since the proof will neither be more certain nor more understandable.) So given that we understand exactly what the computer is verifying in its part of 4CT, and given the extreme difficulty of Wiles' proof, I suggest that the 4CT proof is more understandable than the FLT proof. Steve Cook

**Follow-Ups**:**Joe Shipman**- FOM: Re: understanding computer proofs

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]