Computation, Proof and Conjecture
Tymoczko's claims about the non-surveyablity of the 4CT are perhaps his most controversial. Surveyability is an important, though fuzzy notion. (It was discussed in the last chapter.) We can survey a proof when it's short and easy to grasp. But when a proof is much longer and more complex, we lose our grip; it ceases to be surveyable. All traditional proofs are surveyable - perhaps not by everyone, but at least by those with the appropriate skill and training. However, in the case of the 4CT, the proof is so long and complex that no human can grasp it. It goes without saying, therefore, that no human could double-check the proof to see if it is mistake-free. Putting these points together, Tymoczko concludes that computer proofs are something new on the mathematical landscape. It's a new way of doing mathematics, a way that makes mathematics empirical, probabilistic, and generally more like the inductive natural sciences.
Of course, mistakes in calculation are commonplace. Some mathematicians even take pride in being poor at simple arithmetic, just as some writers brag about their inability to spell. But this sort of mistake is not what Tymoczko has in mind. Ptolemy was wrong, and so was Newton, but not because they made calculation errors. Their mistakes are the mistakes of empirical science - false hypotheses. The fallibility of computer proofs stems from this source. We hypothesize certain things about a computer and about the software that it's running. And this hypothesis may be wrong. Greater use of the machine in a variety of circumstances and greater testing of the software (or fragments of it) can lead to greater confidence, but it will never leave us with anything better than a well-confirmed scientific theory.