qed applied to four color theorem

John McCarthy (jmc@sail.Stanford.EDU)
Tue, 1 Nov 1994 11:42:24 -0800

The 1979 proof of the four color theorem involved at least two very
large computer programs. One of them showed that each of 1936 graph
configurations was reducible and therefore could not occur in a
minimal counterexample to the theorem. The other program showed that
every (standardized) map graph contains at last one of the 1936

Mathematicians doubted the correctness of these programs. If I recall
correctly, the referees wrote some of their own programs.

These programs, or new programs that perform the same tasks, would be
very suitable for qed verification and very likely would impress