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