FOM: Computer-aided proofs

[JoeShipman@aol.com]

A proof of the Kepler conjecture, the oldest unsolved problem in mathematics
(it states that the standard packing of spheres in 3-space attains the best
possible asymptotic density), has been announced by Thomas Hales of the
University of Michigan.  The proof involved heavy interaction between
mathematicians and computers.  Details are at 
http://www.math.lsa.umich.edu/~hales  .

In the 4-color theorem of Appel and Haken, the computer-aided proof comprises
the following:
-- An algorithm (for 4CT, check a given set of configurations for
unavoidability and reducibility)
-- Input data for the algorithm (for 4CT, a couple of thousand configurations)
-- A conventional (non-machine-aided proof) that if the algorithm has a
specified output for some input data then the theorem is true. (This was the
bulk of the 4CT paper as published in the Illinois Journal of Math in 1976;
the input data was a special microfilm insert on the inside back cover of the
journal issue.)
-- A description of a computational system in which the algorithm was
implemented, along with details of the implementation 
-- An assertion (possibly including some computer "trace" output) that this
implementation of the algorithm produced the desired output.

The situation with Hales's proof of the Kepler conjecture appears to be
analogous, except that each piece appears to be quite a bit more complex than
the corresponding piece in the Appel-Haken proof of the four-color theorem.

4CT was "verified" quickly because the algorithm was straightforward enough,
and the input data manageable enough, that independent researchers could write
their own implementations and check the outputs.

But it is widely underappreciated how difficult and dangerous verification is.
For a hilarious horror story, read how Thomas Nicely of Lynchburg College
discovered the flaw in the Pentium chip while trying to calculate some
constants related to the distribution of twin primes ("Enumeration to 1e14 of
the twin primes and Brun's constant", Virginia Journal of Science, Volume 46,
Number 3 (Fall 1995), pp.195-204, available online at 
http://www.lynchburg.edu/public/academic/math/nicely/twins/twins.htm ).

The following quote from this paper summarizes the lessons Nicely learned:

<<<<<
After this tempest began to settle (mathematicians in general, and this one in
particular, are not accustomed to being besieged by inquiries and visits from
network news, the BBC, the Washington Post, the Wall Street Journal, and the
New York Times, as well as journalists from France, Australia, and Malaysia),
attention returned to the work at hand. With commendable haste, Intel provided
a replacement chip for the errant Pentium (as well as one for a colleague's
system) and also supplied a 90-MHz Pentium system to help make up for lost
time. Naturally, all remaining calculations were carried out in duplicate, and
the wisdom of this caution was confirmed when other discrepancies appeared
between duplicate runs. Twice the errors were tracked to intermittently
defective memory (SIMM) chips; parity checking had failed to report either
error. On another occasion, a disk subsystem failure generated a wholesale lot
of incorrect, yet plausible data. In the most recent instance, a soft memory
error appears to be the culprit. 

Although many may dismiss machine errors such as these as of no practical
consequence (except to mathematicians) or as evidence of the unreliability of
personal computers, I believe there is a more important conclusion to be
drawn. Any significant computation, for which there is no simple check
available, should be performed in duplicate, preferably on two different
systems, using different CPUs, hardware, operating systems, application
software, and algorithms. In practice, it is difficult to obtain this degree
of independence; but certainly, one must be suspicious of the result of any
single, lengthy machine computation, whether it is performed on a personal
computer or the world's finest supercomputer. As we tell our students---check
your work! 
>>>>>

The five different levels Nicely recommends duplicating (CPU, hardware,
operating system, application software, and algorithms) all experienced
failures at different stages of the project, and of course only the last of
these five was his fault!

In the absence of rigorous proofs of the correctness of computer systems
(including chip design, programming language, compiler, and operating system),
we can not have the same type of certainty about the correctness of a
computer-aided proof as we can of a humanly surveyable proof.  But we can
attain "moral" certainty if we follow Nicely's recipe with sufficient
thoroughness (I would demand more than two verifications in which all the
components of the system were independent for an important result like 4CT or
the Kepler conjecture).  

"Conventional" proofs are not always more certain than this.  Three
illustrations:
1) Smale's paper on "Problems for the 21st Century" in the Spring 1998
Mathematical Intelligencer (which I recommended to FOM a few months ago)
mentions in passing a shockingly large number of incorrect "theorems" which
were originally accepted and took years to be recognized as not really proved
2) Hsiang's 1990 "proof" of the Kepler conjecture, a consensus against which
was obtained only several years later (the paper still has not been withdrawn)
3) The classification of finite simple groups is said to be several thousand
pages long and I do not believe any single mathematician has carefully checked
the entire thing; thus no one can have the confidence that this theorem is
true that they can have about a proof they have personally checked, everyone
can have only the confidence attainable from accepting the authority of other
mathematicians, which is less.  (I'm not even sure every piece of the proof of
the Classification has been validated by several referees yet -- does anyone
know if this has yet occurred?)  For example, I have personally verified
proofs of the Prime Number Theorem and Godel's Incompleteness Theorem; I
depend on the authority of other mathematicians for my belief in Wiles's
("Fermat's Last") Theorem and Friedman's latest independence results, though I
look forward to one day personally verifying them.

-- Joe Shipman