Abstract
The subject of this thesis is mathematical proof involving the use of computers. The proof in 1976 of the Four-Colour Theorem, in which an essential lemma is proved using a computer program which took over 1200 hours of computer time to complete, raises philosophical questions concerning the epistemological status of the proof and the extent to which its acceptance as a proof effects an alteration in the traditional concept of mathematical proof. Section I provides an exposition of this proof and a discussion of the Kantian conception of a priori knowledge to provide a background for the following analysis of the philosophical controversy which immediately developed after the publication of the proof. The unsurveyable length of the proof gave rise to the view that its structure was fundamentally empirical and closer to a scientific experiment than a traditional a priori proof. Objectors to this view claimed that the proof differed from most others only in that its empirical content was greater. No essential qualitative difference was involved. These views are examined, and an analysis of those of Frege and J.S. Mill are used to support the opinion that a detailed reassessment of the a priori/a posteriori distinction is necessary to clarify the issues raised by this type of proof. Section II provides an account of recent developments in epistemology with particular reference to the a priori/ a posteriori distinction and favours an analysis of this distinction based on differences in types of psychological process required to generate knowledge. It is maintained that this type of "psychologistic" analysis provides a clarification rather than a rejection of the Kantian conception of the distinction and shows clearly that the Four-Colour Theorem does significantly differ from previous purely formal proofs. _ The conclusion is that acceptance of unsurveyably long computer proofs by the mathematical community involves relinquishing a characteristic of proof formerly held to be essential.