There are many sources of potential errors: wrong inputs, programming mistakes, undetected bugs in the compilers and hardware errors such as the random changing of bits in the computer’s memory. If anything, we can be almost certain that some error did occur. It should be clear why it is impossible to verify the correctness of this proof. We could perhaps check all the computer programs there are also the compilers and operating systems to reckon with, but how are we to guarantee the absence of built-in hardware errors or random errors during a run? As for trying to simulate the workings of the supercomputer by hand, the enormity of the task staggers the imagination: the actual search took more 2000 hours of computer time-at a rate of hundreds of millions of operations per second.
We may establish the validity of the result-if not the absence of errors-indirectly, for example, by an independent verification, using different programs and machines. Another such test is the test of time. It is a simple but fundamental logical principle that from a false premise we can prove anything. If the four-color theorem is false but believing it true we use it to prove other theorems, one of these may contradict some well-established fact. Should no such contradiction ever happen, this would add weight to the computer result.
Surely the use of computers in proofs introduces an element of uncertainty new to mathematicians but not to experimental scientists. This seems a small price to pay for the use of such a marvelous tool. A central issue is the question of the length of proofs. The shortest proofs of some mathematical propositions are much too long for any human being to check in full. Admittedly, we do not know whether there are any important or interesting theorems in this category.
A computer assisted proof would be like the picture of a peak on some distant planet transmitted by a space probe. Our observer may reject this electronic image as unreliable, second-hand evidence. Real mathematicians are in a similar predicament when confronted with a proof by computer. They may postpone accepting the result until someone comes up with a shorter proof, a proof they could check themselves. But they realize that such a proof may be impossible. And so, if they reject the indirect evidence, they risk being cut off from a mathematical truth accessible only by nontraditional means.
We may establish the validity of the result-if not the absence of errors-indirectly, for example, by an independent verification, using different programs and machines. Another such test is the test of time. It is a simple but fundamental logical principle that from a false premise we can prove anything. If the four-color theorem is false but believing it true we use it to prove other theorems, one of these may contradict some well-established fact. Should no such contradiction ever happen, this would add weight to the computer result.
Surely the use of computers in proofs introduces an element of uncertainty new to mathematicians but not to experimental scientists. This seems a small price to pay for the use of such a marvelous tool. A central issue is the question of the length of proofs. The shortest proofs of some mathematical propositions are much too long for any human being to check in full. Admittedly, we do not know whether there are any important or interesting theorems in this category.
A computer assisted proof would be like the picture of a peak on some distant planet transmitted by a space probe. Our observer may reject this electronic image as unreliable, second-hand evidence. Real mathematicians are in a similar predicament when confronted with a proof by computer. They may postpone accepting the result until someone comes up with a shorter proof, a proof they could check themselves. But they realize that such a proof may be impossible. And so, if they reject the indirect evidence, they risk being cut off from a mathematical truth accessible only by nontraditional means.
RSS Feed
