Re: [HM] Proofs and the computer

Samuel S. Kutler (s-kutler@sjca.edu)
Tue, 8 Jun 1999 17:56:08 +0100

Emmanuel:

You wrote

> The famous 4-colour problem took more or less a hundred years to
> be "solved" after several intelligent and creative attempts.
> However, the "proof" required the helping hand of the computer.
> I once heard the question "How are we to prove the correctness of
> the program?"

We can't prove its correctness, but think of Wiles's proof of Fermat's Last
Theorem:

How can we prove its correctness?

We've had fine number theorists go over it with a metaphorical fine-toothed
comb.

With the 4 color program, perhaps the most effective way is to have a new
team of programmers under the direction of mathematicians re-program it
from scratch to try to obtain the same result.

Best wishes,

Sam Kutler