FOM: understanding computer proofs

[Stephen Cook]

I enjoyed reading Joe Shipman's December 7 illuminating discussion of
the three big theorems, including his notions of the depth, width, and
length of proofs.

Here I want to comment on one aspect of his Dec 11 discussion of
mathematical certainty, namely his suggestion that Wiles' proof of FLT is more
understandable than the recent computer-aided proof of 4CT.  Joe argues
that the "mathematical" protion of the 4CT proof is quite well 
established, and many people understand it.  However, the computer
part "...depends on so many finite combinatorial `facts' that we still
need to point to a computer output to persuade someone else that it
is true".

It seems to me that in general, if the use of a computer in a proof
involves only straightforward, understandable algorithms, then the
reliance on the computer does not degrade the understandability of
the overall proof (or at least not much).  To make this point, suppose
that a hypothetical proof of an important result relies on verification
that a certain number p is prime; say p is 8 or 10 digits long.
Suppose that the verification can be carried out in an hour, using
a pocket calculator for integer arithmetic, or in ten hours using
long hand arithmetic with no mechanical aids.  It seems to me that
there is no increase in understanding gained by doing the arithmetic
by hand.  (In fact I wonder if there is any reason at all to do the
arithmetic by hand, since the proof will neither be more certain nor
more understandable.)

So given that we understand exactly what the computer is verifying in
its part of 4CT, and given the extreme difficulty of Wiles' proof,
I suggest that the 4CT proof is more understandable than the FLT proof.

Steve Cook