Newsgroups: comp.risks X-issue: 8.70 Date: Thu, 11 May 89 03:18:49 EDT From: henry@utzoo.UUCP Subject: Computers in mathematical proofs The March 1989 Scientific American has a very interesting little piece in its "Science and the Citizen" column, talking about the growing acceptance of computerized proofs in mathematics. It cites the 1976 Haken/Appel proof of the four-color theorem, and the controversy that followed, but observes that at least in principle, that result could be checked by hand. Now we have a significant proof for which hand checking is out of the question: Clement W.H. Lam of Concordia University has used 3000 hours on a Cray-1, spread over two years, proving an instance of one of Gauss's conjectures ("there are no finite projective planes of order 10", to be precise). This proof, unlike the Haken/Appel one, is meeting little opposition, despite its complexity (100 trillion cases) and the fact that it was done with a collection of small programs rather than a single systematic large one. Lam himself says he was hoping for a positive result, which would be easy to check, rather than a negative one. But he is fairly confident in his result, citing two reasons: (a) the programs did do some internal consistency checks; (b) the result agrees with "mathematical intuition" (for example, an order-10 projective plane is known to be forbidden to have any symmetry, which apparently is almost unheard-of for such an object). Mathematicians are coming to accept computers, it seems. Ronald L. Graham of Bell Labs observes that nobody has flatly refused to accept Lam's result, as some did for the Haken/Appel result. Haken himself observes that there is a more mundane explanation for that: many of the objectors were older mathematicians who have since retired. Haken and Graham both observe that "simple theorems should have simple proofs" is a religious belief rather than a law of nature, and is verifiably false in some simple artificial mathematical systems. Henry Spencer at U of Toronto Zoology

Index Home About Blog