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