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

*To*: Stephen Cook <sacook@cs.toronto.edu>*Subject*: FOM: Re: understanding computer proofs*From*: Joe Shipman <shipman@savera.com>*Date*: Mon, 14 Dec 1998 13:05:04 -0500*CC*: fom@math.psu.edu*Organization*: Savera systems*References*: <98Dec14.105829edt.37768-4373@qew.cs.toronto.edu>*Sender*: owner-fom@math.psu.edu

Stephen Cook wrote: > 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. This very point occured to me when I was writing my previous post, and I wondered whether Wiles's proof required even this much "numerical work". I was assuming that it didn't. I agree that reliance on the computer doesn't degrade the understandability of a proof much; but the degree to which it does is proportional to the amount of work involved, which is much larger than verifying that a 10-digit number is prime and could not be feasibly carried out by a person. "x is prime" for some 10-digit x, while requiring a significant amount of work to verify, is an understandable statement; in the same way, "Y is reducible", where Y is one of Appel and Haken's 2000 configurations, is an understandable statement. But if a proof depended on the primality of a couple of thousand 10-digit numbers, and there was no shortcut to testing all of them, it would be fair to say that the proof is not fully "understandable". Understandability depends on the reader. The top 20 or 30 algebraic number theorists in the world probably understand Wiles's proof in a very strong sense (they could reproduce it, filling in as much detail as is demanded) and would not be willing to say they "understood" the proof of 4CT as well even if they had independently written programs to verify the two computer-aided lemmas. Most of the rest of us probably do find the 4CT proof more understandable than the FLT proof, even if we could follow the FLT proof in some detail, but it seems fair to say that no one understands the 4CT proof as well as those 20 or 30 people understand the FLT proof, and it is this "maximum attainable degree of understanding" that I am interested in. -- Joe Shipman

**References**:**Stephen Cook**- FOM: understanding computer proofs

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

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