FOM: Re: 4CT vs FLT

[Michael Thayer]

-----Original Message-----
From: Stephen Cook <sacook at cs.toronto.edu>
To: fom at math.psu.edu <fom at math.psu.edu>
Cc: sacook at cs.toronto.edu <sacook at cs.toronto.edu>
Date: Wednesday, December 02, 1998 11:25 AM
Subject: FOM: 4CT vs FLT


>
>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?
>
For what it is worth, there are two separate programs afoot to rework this
proof into more reasonable form: many earlier results can have much
shortened proofs due to later findings.  It is hoped that the result may be
only ~2000 pages.  Some results have not been shortened, for instance the
famous Feit -Thompson result which caused the big push on the Brauer program
in the 60's.

The main conviction added by these current programs will probably be that
the teams involved will have gone over the entire proof when completed.  But
what does all this mean?  How many people read Herbrand's proof without
findinf the error that Dreben et al. repaired in the early 60's (30 years
after original publication).

Maybe computer proofs are less convincing to some for the reasons that
Sazanov has given: they are not readily understandable arguments as to the
existence of a formal proof.

Michael Thayer