From owner-qed Tue Nov 1 13:42:55 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id NAA04886 for qed-out; Tue, 1 Nov 1994 13:42:32 -0600
Received: from SAIL.Stanford.EDU (SAIL.Stanford.EDU [36.28.0.130]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id NAA04881 for ; Tue, 1 Nov 1994 13:42:26 -0600
Received: by SAIL.Stanford.EDU (5.65/25-SAIL-eef) id AA26526; Tue, 1 Nov 1994 11:42:24 -0800
Date: Tue, 1 Nov 1994 11:42:24 -0800
From: John McCarthy
Message-Id: <9411011942.AA26526@SAIL.Stanford.EDU>
To: qed@mcs.anl.gov
Subject: qed applied to four color theorem
Reply-To: jmc@cs.stanford.edu
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
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.