>  > [log in to unmask] writes:
>  >
>  > However it does indicate that there can be no possibility
>  > of a computer program ever correctly claiming that it has
>  > found a proof that differs from a mathematiocal proof. 
And in a message dated 3/12/01 10:36:21 AM EST, [log in to unmask] writes:

>  Where does this leave the computer "proof" of the 4 color theorem? Doesn't 
>  the absence of a mathematical proof  indicate that the computer proof 
>  "differs" from the (non-existant) mathematical proof?

   It **isn't** that the mathematical proof was "nonexistent". It was that 
the mathematicians had reduced the proof to the separate examination of 
thousands of individual cases. The "math" part is in proving that when you 
consider each of the gazillion cases, there are no other cases to consider. 
The "computer" part is in examining each of the gazillion cases separately, 
and quickly (compared to human examiniation time).

As the article I quoted earlier states:

"The proof was achieved by Appel and Haken, basing their methods on 
reducibility using Kempe chains. They carried through the ideas of 
Heesch and eventually they constructed an unavoidable set with around 
1500 configurations."

   To examine each of the possible number of cases, even though the number of 
cases is finite, would take human beings a gazillion years to do. The 
computer was able to "examine" each and every case in 1200 hours. When the 
program had finished running, there were no other cases to consider, and each 
of the maps under consideration had been drawn with only four colors. Thus, 
the four-color map theorem had been proved.  

-- Steve --