> > [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 --