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.