Xref: utzoo comp.theory:845 sci.logic:881 sci.math:11678
Path: utzoo!attcan!uunet!convex!texsun!newstop!sun-barr!cs.utexas.edu!usc!rutgers!netnews.upenn.edu!grad2.cis.upenn.edu!aaron
From: aaron@grad2.cis.upenn.edu (Aaron Watters)
Newsgroups: comp.theory,sci.logic,sci.math
Subject: Re: Re^4: Question About the Four Color Proof
Message-ID: <27018@netnews.upenn.edu>
Date: 12 Jul 90 20:02:29 GMT
References: <786@qusunu.queensu.CA> <9615@hubcap.clemson.edu> <1212@s8.Morgan.COM> <9649@hubcap.clemson.edu>
Sender: news@netnews.upenn.edu
Reply-To: aaron@grad2.cis.upenn.edu.UUCP (Aaron Watters)
Organization: University of Pennsylvania
Lines: 14

In article <9649@hubcap.clemson.edu> steve@hubcap.clemson.edu ("Steve" Stevenson) writes:
>
>... my interest is in the fact that a computer program is
>involved. In the philosophical sense, has FCT been `proven' if it has an
>`unproven' computer program in the middle?

What makes you think that the program is any more or less proven
than other parts of this or other proofs?  The algorithm is certainly
not `unproven' by normal standards of mathematical discourse.  If
your problem is with the possibility of an implementation mistake
or a hardware error in the execution, I'd say this is much less likely
than the possibility of an ordinary mathematical nonsequitur in the
main part of the proof, especially since the algorithm has been
reimplemented and rerun.		-aaron.