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.