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