Computers and Mathematical Proofs

Apparently, mathematicians take a dim view of the use of computers in proving theorems. This blog post from the Heidelberg Laureates Forum gets a mathematician to articulate why:

Efim Zelmanov spoke up first, saying, “A proof is what is considered to be a proof by all mathematicians, so I’m pessimistic about machine-generated proofs.” He mentioned the four-color theorem, which was the first major proof to be solved using a computer, in 1976. One hundred twenty-four years after it was first proposed, Kenneth Appel and Wolfgang Haken cleverly reduced the problem to checking the properties of 1,936 maps by computer. The result was hundreds of pages of hand analysis combined with thousands of lines of computer code. Many mathematicians hated this, not accepting the proof because it was impossible to check by hand. Michael Atiyah chimed in with a similar perspective: “We aim to get understanding in mathematics,” he said. “If we have to rely on an unintelligible computer proof, it’s not satisfactory.”

Here's another story from 2004 on the proof of Kepler's Conjecture on "the most efficient way to pack oranges":

A leading mathematics journal has finally accepted that one of the longest-standing problems in the field -- the most efficient way to pack oranges -- has been conclusively solved.

That is, if you believe a computer.

The answer is what experts -- and grocers -- have long suspected: stacked as a pyramid. That allows each layer of oranges to sit lower, in the hollows of the layer below, and take up less space than if the oranges sat directly on top of each other.

While that appeared to be the correct answer, no one offered a convincing mathematical proof until 1998 -- and even then people were not entirely convinced.

For six years, mathematicians have pored over hundreds of pages of a paper by Dr. Thomas C. Hales, a professor of mathematics at the University of Pittsburgh.

But Dr. Hales's proof of the problem, known as the Kepler Conjecture, hinges on a complex series of computer calculations, too many and too tedious for mathematicians reviewing his paper to check by hand.

Believing it thus, at some level, requires faith that the computer performed the calculations flawlessly, without any programming bugs. For a field that trades in dispassionate logic and supposedly unambiguous truths and falsehoods, that is an uncomfortably gray in-between.

See also: Dana Mackenzie in The American Scientist: The Proof is in the Packing.