Topics Mathematics

Question It was said [in a Google groups <A href="http://groups.google.com/group/AskPhilosophers/browse_frm/thread/711d9119ce7b33c3?tvc=1&q=computer" target="_blank">post</A>] that "If a [mathematical] proof requires the checking of a very large but finite number of cases, far too many for a human to check, and we use a computer to perform that check, should we count the proposition as proved?" is an open question of mathematical philosophy. Why would anyone think the answer is anything but "yes"? The proof may not have desired aesthetic qualities, but no mathematician would deny its validity even though she may try to create a more pleasing proof.

Accepted:
November 6, 2005

Comments

It depends on what you think a proof is supposed to be. If you think a proof is just a certain kind of abstract object--say, a finite arrangement of symbols that satisfies the rules of logic--then it seems that a computer-checked proof is a proof just as much as a human-checked proof is.

But another way of looking at it is to think about the role proofs play. When you read and understand a proof, you become convinced that a certain mathematical statement is true, and the proof is what convinces you. Now, suppose you are convinced by a computer-checked proof--say, the proof of the 4-color theorem. What is it that convinced you that the 4-color theorem is true? Not the proof that the computer checked--you never saw that proof, and it's far too long for you to read yourself. No, what convinced you of the truth of the 4-color theorem is a certain physical experiment: connecting a box full of wires to a source of electricity and seeing what happens. It seems that your belief in the 4-color theorem relies on your belief in not only the laws of logic, but also the laws of electronics, which are empirical. You also have to be convinced that the program was correct. Should the proof of the theorem include a proof of the correctness of the program? These kinds of concerns don't seem to come up when we judge whether or not ordinary, human-checked proofs are convincing.

One possible response to these worries is that this situation is no different, in principle, from the situation in which you believe a theorem because you trust your mathematical colleague, who assures you that he has checked the details of the proof. But in that case at least your colleague's belief in the theorem is based on understanding the proof itself, even if yours isn't. Does it matter if no human being ever understands a proof?

A related but different issue concerns computations that do not produce proofs, but do give us good reason to believe something. For example, there are calculations that can be used to show that a number p is very likely to be prime. The calculation is not a proof that p is prime, because it does not establish that p is prime with certainty. But in practice the reliability of such calculations can be made very high--just as high as the reliability of human-checked proofs, which after all are subject to error, since humans make mistakes. Should mathematicians begin trusting such calculations to answer mathematical questions, or should they insist that a question isn't settled until there is a proof?

A few references:

Thomas Tymoczko, The Four-Color Problem and Its Philosophical Significance, Journal of Philosophy, Vol. 76, No. 2, Feb. 1979, pp. 57-83, reprinted in New Directions in the Philosophy of Mathematics, Princeton Univ. Press.

John Horgan, The Death of Proof, Scientific American, Oct. 1993

Steven Krantz, The Immortality of Proof, Notices of the Amer. Math. Soc., Jan. 1994. (This is a response to Horgan.)

I don't have anything to add to Dan's comments, which pretty much cover the bases. But I will add another reference: Tyler Burge, "Computer Proof, A priori Knowledge, and Other Minds", Philosophical Perspectives, vol. 12, pp. 1-37, 1998. Burge's discussion ties the question asked here to very general questions about the nature of a priori knowledge.