FOM: Re: understanding computer proofs

[Joe Shipman]

Stephen Cook wrote:

> 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.

This very point occured to me when I was writing my previous post, and I wondered
whether Wiles's proof required even this much "numerical work".  I was assuming
that it didn't.  I agree that reliance on the computer doesn't degrade the
understandability of a proof much; but the degree to which it does is proportional
to the amount of work involved, which is much larger than verifying that a
10-digit number is prime and could not be feasibly carried out by a person.

"x is prime" for some 10-digit x, while requiring a significant amount of work to
verify, is an understandable statement; in the same way, "Y is reducible", where Y
is one of Appel and Haken's 2000 configurations, is an understandable statement.
But if a proof depended on the primality of a couple of thousand 10-digit numbers,
and there was no shortcut to testing all of them, it would be fair to say that the
proof is not fully "understandable".

Understandability depends on the reader.  The top 20 or 30 algebraic number
theorists in the world probably understand Wiles's proof in a very strong sense
(they could reproduce it, filling in as much detail as is demanded) and would not
be willing to say they "understood" the proof of 4CT as well even if they had
independently written programs to verify the two computer-aided lemmas.  Most of
the rest of us probably do find the 4CT proof more understandable than the FLT
proof, even if we could follow the FLT proof in some detail, but it seems fair to
say that no one understands the 4CT proof as well as those 20 or 30 people
understand the FLT proof, and it is this "maximum attainable degree of
understanding" that I am  interested in.

-- Joe Shipman