My impression of this debate is that the computer gives a proof in the sense of a certificate of truth, at least as reliable as those produced by humans. But that what we often want in a "proof" is a sense of _why_ something is true --- this is why we often try to find multiple proofs of the same thing, and why we want "proofs from the book". It seems we don't yet have this kind of proof for the 4-color theorem. On the other hand, I have heard (does anyone have a reference?) that while God has a book of the most elegant and insightful proofs, the Devil has a book of mathematical truths that are easy to state, but which have no proof in God's book. Perhaps the 4-color theorem is one of these... Cris On Apr 29, 2013, at 11:37 AM, Robert Baillie wrote:
I never saw what the big deal was about this computer proof.
For many years before 1976, computers had been the only entities that were capable of verifying the primality of large Mersenne numbers.
Bob Baillie