The most familiar to research mathematicians is the role of verification. A statement can be treated as belonging to the body of mathematics only when it has been verified. The proof should not only show that a given sentence is true and holds but should also explain why it is true and holds. This role explains why mathematicians are often looking for new proofs of known theorems – newproofs should have more explanatory power. The role of systematization was exemplified already by Euclid’s Elements. In this work, many theorems known to Greeks have been collected and organized in such a way that they followed from axioms, postulates, definitions and previously proved theorems. It was shown in this way that the accepted axioms, postulates and definitions form a sufficient base on which the whole edifice of mathematics can be developed. Note that the role of discovery may be – prima facie – rather seldom associated with proofs but it is not excluded. In fact, e.g. non-Euclidean geometries were arrived at through purely deductive means. Recall that since Euclid one asked the question whether the fifth postulate on parallels formulated in Elements is independent of other axioms and postulates or can be deduced from them. After several attempts undertaken through the centuries, it has been shown in the 19th century that it is reasonable to consider systems of geometry in which the negation of the fifth postulate is assumed instead of the fifth postulate itself, and it is possible to show that such systems are consistent.
Finding proofs is the intellectual challenge for mathematicians: there is a theorem – we want to prove it. Proofs serve in the community of mathematicians as communication means. They communicate not only the reasons why a given statement is a true theorem but introduce also new methods which can be used sometimes in other domains. Proofs can provide also justification of definitions.
The most important roles played by proofs in the research mathematical practice are of course verification and explanation. Note that a proof that verifies a theorem does not have to explain why it holds. One can distinguish between proofs that convince and proofs that explain. The former should show that a statement holds or is true and can be accepted, the latter – why it is so. Of course, there are proofs that both convince and explain. The explanatory proof should give an insight in the matter whereas the convincing one should be concise or general. One can distinguish also between explanation and understanding. Mathematicians←41 | 42→often treat simplicity as a characteristic feature of understanding. Observe that, as G.-C. Rota writes in (1997, p. 192):
[i]t is an article of faith among mathematicians that after a new theorem is discovered, other, simpler proof of it will be given until a definitive proof is found.
In this context, it is worth distinguishing between unveiling proofs and consolidating ones. The former one is “a proof which proves a theorem which was unknown before” and the latter is “a proof of a theorem which is already known to be true” (Kahle 2015). Proofs of the second type do not contribute to the truth of a theorem – they consolidate our knowledge of this truth. Such a proof can be quite different from the original one. Aschbacher wrote about this phenomenon in the following way (2005, p. 2403):
The first proof of a theorem is usually relatively complicated and unpleasant. But if the result is sufficiently important, new approaches replace and refine the original proof, usually by embedding it in a more sophisticated conceptual context, until the theorem eventually comes to be viewed as an obvious corollary of a larger theoretical construct. 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