Thus proofs are a means for establishing what is real and what is not, but also a vehicle for arriving at a deeper understanding of mathematical reality.
There are many examples from the history of mathematics that confirm this. In this context, one can mention Paul Erdős’ idea of proofs from The Book in which God maintains the perfect proofs for mathematical theorems – he followed the dictum of G.H.Hardy that there is no permanent place for ugly mathematics. Erdős stressed that one need not believe in God but, as a mathematician, one should believe in The Book.23
Note that a proof that convinces can be more (or even quite) formal. Explanatory proofs cannot be strictly formal. Mathematicians set a high value on explanatory proofs. Such a proof is more valued when “it exhibits methods that are powerful and informative” (Avigad 2006, p. 106).Hersh says in (1997, p. 60) that “[p]roof is a tool in service of research, not a shackle on the mathematician’s imagination”.24
Sometimes theorems are verified in mathematics by checking all particular cases, but this usually does not give an explanation why the theorem holds. The explanation should give a general principle by which the theorem holds. a famous example of a theorem verified by checking cases but not giving reasons is the Four-Color Theorem proved by Appel and Haken and stating that every planar graph is four-colourable, i.e. in another words, that four colours suffice to colour everymap ←42 | 43→on the plane in such a way that two regions receive different colours whenever they have a common border.
The example of the Four-Color Theorem indicates other features of proofs in mathematics. Observe that the first purported proof of it given by Kempe in 1879 was accepted for a decade before it was found to be incorrect. This was neither the first nor the last example of such a situation. It means that the community of mathematicians can be fallible.
The Four-Color Theorem opened eyes of philosophers of mathematics to the problem of methods acceptable in a proof or in a verification of cases. The unique known proof – that by Appel and Haken – was obtained by using computer, and no traditional proof (without computer) is known so far. Moreover, the existing proof cannot be made by a human being because an essential part of it was a computation requiring about 1200 hours of computer time and is beyond the capacities of any mathematician. This initiated a discussion concerning the admissibility of experimental methods in mathematical proofs. Several arguments pro and contra have been formulated – we will not enter here the details of the discussion. Let us say only that the usage of a technical tool (like a computer) seems to refute the commonly accepted thesis that mathematical knowledge is a priori. There arises also a question whether a computer-aided proof is (or can be treated as) a mathematical proof and consequently, whether in particular the Four-Color Theorem can be called “theorem” or it is still rather a hypothesis.
In this debate initiated by a paper by Tymoczko (1979) a question was asked what are in fact the characteristic features of a “normal”mathematical proof. Tymoczko says that a proof in mathematics should be: (1) convincing, (2) surveyable and (3) formalizable.
The first feature is – as Tymoczko says – of an “anthropological” character, the other two are treated by him as “deep features”. He claims also that “surveyability and formalizability can be seen as two sides of the same coin” (Tymoczko 1979, p. 61). Formalizability “idealizes surveyability, analyzes it into finite reiterations of surveyable patters” (ibidem). It can be assumed that all surveyable proofs are formalizable. Are also all formalizable proofs surveyable? Tymoczko answers this negatively: “[w]e know that there must exist formal proofs that cannot be surveyed by mathematicians if only because the proofs are too long or involve formulas that are too long” and the phrase “too long” means here “can’t be read over by a mathematician in a human life time” (ibidem). On the other hand, one should observe that “it is not at all obvious that mathematicians could come across formal proofs and recognize them as such without being able to survey them” (Tymoczko 1979, p. 62).
Considering surveyability one should distinguish local and global surveyability. Bassler in (2006, p. 100) characterizes them in the following way:
←43 | 44→
local surveyability requires the surveying of each of the individual steps in a proof in some order, while global surveyability requires the surveying of the entire proof as a comprehensive whole.
Hence, a local surveyability does not mean that a proof is practically surveyable. One can say that the proof of the Four-Color Theorem is globally surveyable without being locally surveyable (provided one is willing to countenance a distinction between proof and calculation). On the other hand, if one accepts the assumption that global surveyability receives its foundation in local surveyability then this statement is false. Add that one should also distinguish the surveyability of a proof and the fact that it can be (formally) checked on the one hand and the fact that it gives an understanding, that it reveals the deep reasons for the theorem being proved on the other.
The concept of surveyability is not precise enough. In the 20th century, there was a trend to link surveyability with the development of formal and complete foundations of mathematics, and formalization was treated as a method providing the local surveyability. The works of Frege, Russell and their followers, especially Hilbert, were guided by the desire to find a perspicuous syntactic representation of the relations of semantic content within a proposition.
Computers and methods connected with them were and are used in mathematics not only in the proof of the Four-Color Theorem. They are used in various contexts in mathematics, in particular: (1) to perform numerical calculations, (2) to find (usually approximate) solutions of equations and systems of algebraic or differential equations or of integrals, (3) in automating proofs of theorems, (4) in checking the correctness of mathematical proofs, (5) in proving theorems (one says then about computer-aided proofs) and (6) in various experiments with mathematical objects (e.g., in the theory of fractals).
From our point of view, the most important applications are (3) and (4) – the application of the type (5) has been discussed above on the example of the Four-Color Theorem.
The automating proving of theorems is connected with the idea of mechanization and automatization of reasoning due to Leibniz (cf. Marciszewski and Murawski 1995). This idea (as one of the factors) led to the development of formal logic and in consequence to the idea of a formal proof.
Formal proofs and their role
Formal proofs were introduced to provide an explication of the informal notion of a proof and to solve some metamathematical problems. They should explain the virtue by which usual proofs used in the research practice are judged to be correct. They should also explain what does it mean that a given statement is a logical or deductive consequence of certain assumptions. As indicated above they ←44 | 45→were introduced in the atmosphere of a crisis in the foundations of mathematics. For Frege and Russell they were means to an end, a way of precisely isolating the permissible proofs and making sure that all use of axioms was explicit. On the other hand, observe that Hilbert was not really interested in actually formalizing proofs and replacing the “normal” research proofs by formalized ones. He treated formalization and formal proofs as a tool to justify mathematics as a science and to establish its consistency. They should serve theoretical purposes – in particular to prove results about mathematics, hence to obtain metamathematical results.
In fact, the development of logic and the concept of a formal proof based only on syntactical properties made possible the development of metamathematics. A lot of interesting results have been obtained here. First of all the old paradigm of mathematics that was functioning since Euclid has been made precise – in fact it has been replaced by a new logico-set-theoretical
