Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!zaphod.mps.ohio-state.edu!unix.cis.pitt.edu!rozin
From: rozin@unix.cis.pitt.edu (R Rozin)
Newsgroups: comp.theory
Subject: Re: Re^4: Question About the Four Color Proof
Message-ID: <26267@unix.cis.pitt.edu>
Date: 26 Jul 90 23:08:08 GMT
References: <786@qusunu.queensu.CA> <9615@hubcap.clemson.edu> <1212@s8.Morgan.COM> <16930@dime.cs.umass.edu> <1236@s8.Morgan.COM>
Reply-To: rozin@unix.cis.pitt.edu (R Rozin)
Organization: Univ. of Pittsburgh, Comp & Info Services
Lines: 16

In article <1236@s8.Morgan.COM> amull@Morgan.COM (Andrew P. Mullhaupt) writes:
>In article <16930@dime.cs.umass.edu>, yodaiken@chelm.cs.umass.edu (victor yodaiken) writes:

 [ ... ]

>> The reason appears to be that any such "proof", using current techniques,
>> would be less obviously correct than the program itself. 

>I cannot possibly see how. 

There is an interesting paper by Knuth, "A simple program, whose proof isn't".
The program is about five lines long, and Knuth says that its correctness
was pretty obvious to him, but when he tried to prove it, it was extremely
difficult.  The proof he gives is several pages long.

Roman Rozin