Computers make it possible for a mathematical proof to run as long as several thousand full-length novels combined. But human beings alone cannot verify such immense proofs. That, according to Ian Stewart, a professor of mathematics at Warwick University, in England, presents "a serious philosophical question" for mathematicians: "Can something be considered a proof if no human can verify it without a computer?"

Chronicle of Higher Education
Friday, March 23, 2007
Jason M. Breslow

For that matter, Mr. Stewart adds, what is a proof, and why are they needed at all?

Traditionally, he writes, "a 'proof' is a series of statements, each following logically from previous statements and a fixed list of axioms." There is no limit to how many logical steps can be involved in a proof. In theory, mathematicians are supposed to verify every single step. But there is a "fundamental tension," Mr. Stewart writes, "between the philosophical definition of a proof -- what mathematicians should do -- and what they actually do."

It would take a lifetime to read through and check each part of a long and complex computer-generated proof, says Mr. Stewart. Even formal proofs generated by mathematicians for the most basic equations can be incomprehensible. He notes that it took Bertrand Russell and Alfred North Whitehead several hundred pages just to formally prove that 2+2=4.

As pragmatists, he writes, "mathematicians are much more interested in solving problems than in philosophizing about their methods." A proof, he writes, is therefore more like a clear set of driving directions. "A list of 10,000 instructions, presented as if they were all equally important, is useless." Instead, he says, "you want the details in places where you are on unfamiliar ground, or where it is easy to take a wrong turn."

In this way, he writes, a proof should function like a narrative. It has to tell a story, "a story told by mathematicians to mathematicians, in a familiar language. If it contains logical gaps, or errors, the readers can -- and eventually will -- notice. That's what they have been trained to do."

[Click here for the rest of the article on-line.]