The article distinguishes two kinds of computer proof: one where the the computer is used to enumerate and check a large number of subcases in a proof, and one where the computer is used to generate a proof via an automated theorem-proving process. The article argues that
It is possible that mathematicians will trust computer-based results more if they are backed up by transparent logical steps, rather than the arcane workings of computer code, which could more easily contain bugs that go undetected.I am skeptical whether mathematicians will be willing to trust a computer over their own intuition. The dark secret at the heart of mathematics is that most proofs are established by ultimately appealing to the reader's intuition. In fact, it is more likely that I can convince a listener of my proof by intuitive arguments than by pure formal methods. This is a sliding scale of course; my intuitively obvious claim is another person's completely nontrivial lemma, and it is through the give and take among mathematicians in the community that a proof is 'stabilized' or 'confirmed'.
Ultimately, it's worth remembering that part of the beauty of mathematics is that rigid formal truths have beautiful intuitive interpretations, and it is these intuitive metaphors that are much more lasting than the proofs themselves.
A quote from the last paragraph of the Economist article is fitting, and would make Timothy Gowers proud:
Why should the non-mathematician care about things of this nature? The foremost reason is that mathematics is beautiful, even if it is, sadly, more inaccessible than other forms of art. The second is that it is useful, and that its utility depends in part on its certainty, and that that certainty cannot come without a notion of proof.
Tags: Economist, proof
"I am skeptical whether mathematicians will be willing to trust a computer over their own intuition."
ReplyDelete(Raises hand) Excuse me?
I'm not. I don't know of a single professional graph theorist who has serious doubts about Robertson, Seymour, and Thomas' proof off the four-color theorem (strangely absent from the Economist article), or any discrete geometer who has serious doubts about Hales' proof of the Kepler Conjecture (except, perhaps, Hsiang). Apparently, the doubts over Appel and Haken's (not "Harken") proof were not aimed at the many cases that were checked by computer, but rather, the actual breakdown into cases, which was done 'by hand'.
Perhaps computer scientists are less willing to accept computer-assisted proofs than most mathematicians, simply because we understand better how difficult it can be to get a computer to do ANYTHING correctly. Computer scientists are notorious Luddites.
Posted by Jeff Erickson