More recently (1994) someone found a way to reduce the number of cases
that had to be checked to something we mere humans could handle; see
http://daisy.uwaterloo.ca/~alopez-o/math-faq/node56.html#SECTION00810000000000000000
So it really is a theorem now, but perhaps more interesting than
the theorem itself is the question of whether a proof by computer
should be considered a proof. If you have ever had the "Aha!"
experience you get when you comprehend a mathematical proof, and you
know with as much certainty as the human mind is capable of that
the statement in question is true, then a proof by computer leaves
some doubt. A supercomputer recently took several hundred hours to
decide that 391581*2^216193-1 is prime. (That's a lot of cycles to produce
one bit of output!) Do you believe that the result is absolutely true?
I heard about some judge in California who would not allow a
mathematician to serve on a jury because "mathematicians do not
understand the concept of proof beyond a reasonable doubt!"
Bill H.
Eva-Lise Carlstrom wrote:
> This is a side point, but I had heard several years ago that the
> four-color problem was now considered solved, and thus it was the
> "four-color theorem" rather than hypothesis or conjecture. So I ran off
> and did a web search in an attempt to confirm this. The answer is in fact
> a bit murky, as it's *apparently* been proven by computer enumeration of
> all possible configurations, but no one knows whether there might be a
> flaw somewhere in the process, as was true of previous human attempts,
> and it took too much processing to be humanly checkable. For anyone who's
> interested, I did find some interesting websites, including
>
> http://sdcc14.ucsd.edu/~fillmore/blurbs/fourcolor/fourcolor.html
>
> which has previous proof attempts, diagrams, and discussion.
>
> --Eva,
> who still has a few coloring books somewhere that are mostly colored in
> using only four colored pencils