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