The Concept of Proof in the Context of a Type-Theoretic Approach, II: Proofs of Theorems

This article is a continuation of the study of the epistemological features of the concept of proof in the context of a type-theoretic approach. The previous article was devoted to epistemology of computer program correctness proofs. It addressed the problems of surveyability of this type of proof, the question of their social role. In turn, this article focuses on the use of various computer tools to prove theorems. The article considers the brute force proofs, briefly examines the general structure of the proof of the four color theorem as proposed by Kenneth Appel and Wolfgang Haken. The most interesting comment about the four color theorem was made by Thomas Tymoczko. His argument concerns the notion of surveyability of proof, and one of the central points is the doubts about the concepts of theorem and proof. According to Tymoczko, the use of computers in obtaining mathematical results leads to the introduction of experimental methods in mathematics. Otto Bradley Bassler emphasizes the concept of an intermediate step and the idea of continuity of thinking in Francis Bacon, Rene Descartes and John Locke. According to Bassler, it is reasonable to distinguish between local and global surveyability. The Appel-Haken proof of the four color theorem is globally observable, but not locally observable. It should be noted that not every mathematician checks absolutely all mathematical results in the process of learning and further work. Proof verification is a social process. If even potential local surveyability cannot be guaranteed, then conviction of the proof is akin to believing in inductive generalizations. The mathematician believes in the correctness of the work of the computer, and this belief turns out to be justified in the spirit of reliabilism. The researcher is convinced of the reliability of the computer. However, this conviction is very complex. Paul Teller expresses an alternative point of view regarding the surveyability of proof. According to Teller, the surveyability of proof constitutes human mathematics, but not mathematics in general. Edwin Coleman expresses a close idea. He points out that practically any proof, if we demand full explication and proof of all intermediate results, will be so long that it will completely go beyond the limits of surveyability. Proofs are surveyable only insofar as they are part of the written archive of mathematical results and rely on the set of intermediate lemmas and theorems that are also included in the “World Mathematical Archive”.

Keywords

Authors

References