 Philosophical discussion of the status of computer proofs was prompted in large part by Appel and Haken’s computer-based proof of the Four Color Theorem in 1976. In his (1979), Tymoczko argues—controversially—that mathematical knowledge based on computer proofs is essentially empirical in character. This is because such proofs are not a priori, not certain, not surveyable, and not checkable by human mathematicians. In all these respects, according to Tymoczko, computer proofs are unlike traditional ‘pencil-and-paper’ proofs. Concerning surveyability, Tymoczko writes: