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

*To*: fom@math.psu.edu*Subject*: FOM: 4CT vs FLT*From*: Stephen Cook <sacook@cs.toronto.edu>*Date*: Tue, 1 Dec 1998 18:16:42 -0500*Cc*: sacook@cs.toronto.edu*Sender*: owner-fom@math.psu.edu

Re: Anatoly Vorobey's posting of Nov 23 on the four-color theorem (4CT) vs Fermat's last theorem (FLT). First let me suggest that among famous theorems proved by mathematicians (without the aid of computers) there is a better example than FLT to illustrate uneasiness with the proof: namely the classification of finite simple groups. I understand that the proof runs to thousands of journal pages, and probably no one mathematician has completely read and checked it all. Is this proof more convincing than the proof, using computers, of 4CT? Now, concerning the 4CT, there is a new and improved version, still using computers, by Neil Robertson, Daniel Sanders, Paul Seymour, and Robin Thomas, Journal of Combinatorial Theory (B) vol 70, pp2-44, 1997. A summary can be found on Thomas' web site: www.math.gatech.edu/~thomas/ The advantages of the new proof over the Appel/Haken proof are that it is simpler, and more importantly it avoids the extraordinary amount of hand checking needed for the Appel/Haken proof. The new proof still makes essential use of computer verification, but at least the non-computer part is clear. The authors discuss the possibility of errors in the proof because of reliance on computers. They say that an independent set of programs was written to do the checking, but no one has proved any of the programs correct. Here is a quote from the web page: ========================================== We should mention that both our programs use only integer arithmetic, and so we need not be concerned with round-off errors and similar dangers of floating point arithmetic. However, an argument can be made that our `proof' is not a proof in the traditional sense, because it contains steps that can never be verified by humans. In particular, we have not proved the correctness of the compiler we compiled our programs on, nor have we proved the infallibility of the hardware we ran our programs on. These have to be taken on faith, and are conceivably a source of error. However, from a practical point of view, the chance of a computer error that appears consistently in exactly the same way on all runs of our programs on all the compilers under all the operating systems that our programs run on is infinitesimally small compared to the chance of a human error during the same amount of case-checking. Apart from this hypothetical possibility of a computer consistently giving an incorrect answer, the rest of our proof can be verified in the same way as traditional mathematical proofs. We concede, however, that verifying a computer program is much more difficult than checking a mathematical proof of the same length. ================================================= DISCUSSION: Concerning the issue of proving the programs correct, I think that even if such proofs were supplied there would still be concerns, because of questions about the operating system and potential hardware errors. I think that the question of believability of the computer results is an engineering question. We gain confidence in the results by knowing that competent people have thoroughly checked the programs under a variety of conditions. A mathematician gains confidence in a published proof by somewhat different, but related, methods. For example, we may check lemmas for special cases, or try relating them to results we are more familiar with. One point of similarity is that the process is gradual, and the checking (in the case of a complicated proof) is probably never completely certain, or at least not until a lot of good mathematicians have checked it over a period of time. Another point of similarity between the published proofs of FLT and 4CT is that most of us will never check the proofs (or programs) directly, and if we believe them at all, it is because of expert testimony. This is certainly an unsatisfactory state of affairs. Anatoly Vorobey uses the Hahn-Banach Theorem as an example of a theorem with an intuitive proof that main-stream mathematicians can understand. Of course it is an important goal to find such proofs for both 4CT and FLT. I like Vladimir Sazonov's recent contribution to the discussion, and I'll comment briefly about it in the next message. Steve Cook

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

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