FOM: 4CT vs FLT

[Stephen Cook]

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