The Four Color Theorem originated in 1850 and was not solved in its entirety until 1976. This report details the history of the proof for the Four Color Theorem and multiple contributions to the proof of the Four Color Theorem by several mathematicians. Ideas such as Kempe Chains, reducibility, unavoidable sets, the method of discharging, and the Petersen Graph are all covered in this report. There is also a brief discussion over the importance of a mathematical proof and how the definition of a proof has changed with the contributions of Computer Science to the mathematical community. / text

Tait showed in 1878 that the Four Color Theorem is equivalent to being able to three-color the edges of any planar, three-regular, two-edge connected graph. Not surprisingly, this equivalent problem proved to be equally difficult. We consider the problem of fractional colorings, which resemble ordinary colorings but allow for some degree of cheating. Happily, it is known that every planar three-regular, two-edge connected graph is fractionally three-edge colorable. Is there an analogue to Tait’s Theorem which would allow us to derive the Fractional Four Color Theorem from this edge-coloring result?

My dissertation focuses on mathematical explanation found in proofs looked at from a historical point of view, while stressing the importance of mathematical practices. Current philosophical theories on explanatory proofs emphasize the structure and content of proofs without any regard to external factors that influence a proof’s explanatory power. As a result, the major philosophical views have been shown to be inadequate in capturing general aspects of explanation. I argue that, in addition to form and content, a proof’s explanatory power depends on its targeted audience. History is useful here, because from it, we are able to follow the transition from a first-generation proof, which is usually non-explanatory, into its explanatory version. By tracking the similarities and differences between these proofs, we are able to gain a better understanding of what makes a proof explanatory according to mathematicians who have the relevant background to evaluate it as so. My first chapter discusses why history is important for understanding mathematical practices. I describe two kinds of history: one that presents a narrative of events, which influenced developments in mathematics both directly and indirectly, and another, typically used in mathematical research, which concentrates only on technical developments. I contend that both versions of the past benefit the philosopher. History used in research gives us an idea of what mathematicians desire or find to be important, while history written by historians shows us what effects these have on mathematical practices. The next two chapters are about explanatory proofs. My second chapter examines the main theories of mathematical explanation. I argue that these theories are short-sighted as they only consider what appears in a proof without considering the proof’s purported audience or background knowledge necessary to understand the proof. In the third chapter, I propose an alternative way of analyzing explanatory proofs. Here, I suggest looking at a theorem’s history, which includes its successive proofs, as well as the mathematicians who wrote them. From this, we can better understand how and why mathematicians prove theorems in multiple ways, which depends on the purposes of these theorems. The last chapter is a case study on the computer proof of the Four Color Theorem by Appel and Haken. Here, I compare and contrast what philosophers and mathematicians have had to say about the proof. I argue that the main philosophical worry regarding the theorem—its unsurveyability—did not make a strong impact on the mathematical community and would have hindered mathematical development in computer-assisted proofs. By studying the history of the theorem, we learn that Appel and Haken relied on the strategy of Kempe’s flawed proof from the 1800s (which, obviously, did not involve a computer). Two later proofs, also aided by computer, were developed using similar methods. None of these proofs are explanatory, but not because of their massive lengths. Rather, the methods used in these proofs are a series of calculations that exhaust all possible configurations of maps.

As computers become a more prevalent commodity in mathematical research and mathematical proof, the question of whether or not a computer assisted proof can be considered a mathematical proof has become an ongoing topic of discussion in the mathematics community. The use of the computer in mathematical research leads to several implications about mathematics in the present day including the notion that mathematical proof can be based on empirical evidence, and that some mathematical conclusions can be achieved a posteriori instead of a priori, as most mathematicians have done before. While some mathematicians are open to the idea of a computer-assisted proof, others are skeptical and would feel more comfortable if presented with a more traditional proof, as it is more surveyable. A surveyable proof enables mathematicians to see the validity of a proof, which is paramount for mathematical growth, and offer critique. In my thesis, I will present the role that the mathematical proof plays within the mathematical community, and thereby conclude that because of the dynamics of the mathematical community and the constant activity of proving, the risks that are associated with a mistake that stems from a computer-assisted proof can be caught by the scrupulous activity of peer review in the mathematics community. Eventually, as the following generations of mathematicians become more trained in using computers and in computer programming, they will be able to better use computers in producing evidence, and in turn, other mathematicians will be able to both understand and trust the resultant proof. Therefore, it remains that whether or not a proof was achieved by a priori or a posteriori, the validity of a proof will be determined by the correct logic behind it, as well as its ability to convince the members of the mathematical community—not on whether the result was reached a priori with a traditional proof, or a posteriori with a computer-assisted proof.

[pt] O advento do uso maciço de computadores em provas matemáticas, ocorrido ao final da década de setenta com a solução de um famoso problema matemático – a prova do Teorema das Quatro Cores – ocasionou disputas filosóficas que ainda hoje demandam esclarecimentos. O objetivo principal da tese consiste em elaborar alguns dos referidos esclarecimentos desde uma perspectiva motivada pela filosofia da matemática de Ludwig Wittgenstein, especialmente no que diz respeito à distinção continuamente manuseada e depurada pelo filósofo ao longo do desenvolvimento de seu pensamento entre provas e experimentos. Após apresentar as principais ideias da prova do Teorema das Quatro Cores em termos históricos, algumas distinções conceituais metodologicamente significativas são elaboradas. A seguir o trabalho analisa, a partir da concepção funcional de a priori de Arthur Pap, o argumento da introdução da experimentação nas matemáticas de Thomas Tymoczko. A leitura das controvérias filosóficas que se seguiram ao argumento de Tymoczko é então apresentada, aplicando-se as distinções conceituais anteriormente elaboradas. Por fim algumas ideias wittgensteinianas sobre da disitinção entre provas e experimentos são exploradas em conexão com a noção de sinopticidade de provas, considerando menos os papéis específicos de tais noções na filosofia da matemática de Wittgenstein, do que investigando as vantagens de suas possíveis aplicações no esclarecimento de tópicos críticos das referidas disputas. / [en] The massive use of computers in mathematical proofs, which started in the end of the seventies trough the solution of one famous mathematical problem – the Four-Color Theorem – entailed philosophical disputes still in need of elucidation. The central aim of this thesis consists in elaborating some of these elucidations from a point of view motivated by Ludwig Wittgenstein’s philosophy of mathematics, mainly in what concerns the distinction between proofs and experiments, which was continuously used and elaborated by the philosopher in the course of the development of his thought. After the presentation of the main ideas involved in the proof of the Four-Color Theorem from a historical perspective, some methodological conceptual distinctions are elaborated. The thesis then shifts to an analysis of the introduction of experiment in mathematics argument, by Thomas Tymoczko, from the point of view of Arthur Pap’s conception of functional a priori. An interpretation of the controversies that followed that argument is developed trough the application of the conceptual distinctions previously elaborated. At last, some wittgensteinian ideas about the distinction between proofs and experiments are explored in connection with the notion of surveyability of proofs, concerned less with its specific roles in Wittgenstein’s philosophy of mathematics than with investigating the advantages of its possible applications in the elucidation of some critical points in the referred controversies.