Skip to main content
SpringerLink
Log in

What is a Proof?

  • Original Paper
  • Published:
Axiomathes Aims and scope Submit manuscript

Abstract

In this programmatic paper we renew the well-known question “What is a proof?”. Starting from the challenge of the mathematical community by computer assisted theorem provers we discuss in the first part how the experiences from examinations of proofs can help to sharpen the question. In the second part we have a look to the new challenge given by “big proofs”.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Notes

  1. One can also attribute the introduction of proofs in philosophical arguments to the Greeks, taking Aristotle’s syllogisms into account.

  2. Of course, Hilbert’s non-constructive proof was by far not the only reason for this discussion, but it played an important role, not least for the personal involvement of Hilbert in this discussion.

  3. Even quite recently there was, for instance, a Discussion Meeting on “The nature of mathematical proof” at the Royal Society, with papers from this meeting published in 2005 in the Philosophical Transactions of the Royal Society A, vol. 363. Also the American Mathematical Society devoted a special issue of the Notices of the Society, volume 55, issue 11, December 2008, to the topic of Formal Proof.

  4. This question was explicitly addressed by Solomon Feferman in a talk at a colloquium in memory of Kurt Schütte in Munich, November 1999.

  5. The question also may be approached from the point of view of category theory, cf. e.g., Lambek (1968, 1969), Došen and Petrić (2004), Straßburger (2005). However, also these approaches are more concerned with the logical structure of a proof, than with the mathematical arguments involved.

  6. Cf. The Pythagorean Proposition of Loomis (1968).

  7. Cf. e.g. Avigad (2006, p. 106), who cites Steiner (1978), Mancosu (2000, 2001) as references to the philosophical discussion of explanation in mathematics.

  8. But, of course, proof search has its merits for specialized problems which are properly modeled, in particular, with respect to applications.

  9. Pedants like to remark here that a proof is always correct by definition—otherwise it would not be a proof. It is obvious that “proof” in the colloquial language includes also alleged proofs, as long as they are not shown to be defective. We assume that the reader has no problems to understand the appropriate meaning of proof from the context.

  10. This observation is the basis of the idea of proof carrying code (Necula 1997). While, in general, it is complicated to check software automatically for correctness, it is much easier to verify the correctness if the software carries already its correctness proof.

  11. This is addressed by Scott when he writes (Scott 2006, p. viiif) with respect to the computer proofs given in Wiedijk (2006): “We can also see clearly from the examples in this collection that the notations for input and output have to be made more human readable.”

  12. For a more elaborated discussion of the issue of checking proofs, see Alama and Kahle (2013).

  13. There is, however, a lot of work in this direction: As examples, we can mention: the LAG project, http://www.cs.man.ac.uk/~petera/LAG/; the Mizar project, http://mizar.org/ and Trybulec (2006); and the Isar extension of the proof system Isabelle, http://isabelle.in.tum.de/Isar/ and Wenzel (1999, 2002), Wenzel and Paulson (2006). Recently, this question was taken up by the Fields medalist Timothy Gowers—attracting a lot of attention in the mathematical communitiy; see, for instance, the paper “A fully automatic problem solver with human-style output” Ganesalingam and Gowers (2013). This paper gives not only an example of such a problem solver, but it also provides an in-depth analysis of the underlying problems.

  14. We propose, as a special instance of the Turing test, to consider theorem provers only as competitive with humans (with respect to the traditional sense of proofs) if an examiner can not distinguish whether (s)he examines a student or a computer which is covered behind a wall. It is an interesting hypothesis, that computers might pass this test for written exams much earlier than for oral exams. If we ask why this could be the case, we see that oral exams can uncover more about the understanding of a proof than written ones.

  15. See Dieudonné (1985, p. 278f).

  16. See Gray (2013, p. 541):

    As he [Poincaré] put it in L’avenir (S&M 22, 373): “In mathematics rigour is not everything, but without it there is nothing.” For Poincaré, a proof is mathematics was enabling; it rested on general ideas capable of wider application (by analogy); it showed not merely that some things are the case, it also explained why some things are the case; [...].

  17. Such a broader understanding includes also heuristic aspects—Poincaré’s productive unity—which, however, we will not discuss in this paper.

  18. The issue of structuring proofs was already addressed by Leron in (1983) and somehow taken up by Lamport in (1995, 2012).

  19. This issue is discussed in Sect. 4 with respect to the proofs of the four-colour theorem, of the Kepler conjecture, of Fermat’s last theorem, and of the classification of finite groups.

  20. These notions are not alternative; in general, generalizing lemmas should also reduce the complexity of a proof.

  21. It is worth citing Bourbaki here (1950, Footnote p. 223):

    Indeed every mathematician knows that a proof has not really been “understood” if one has done nothing more than verifying step by step the correctness of the deductions of which it is composed, and has not tried to gain a clear insight into the ideas which have led to the construction of this particular chain of deductions in preference to every other one.

  22. Based on this view we could actually argue that computers do not understand the proofs they generate.

  23. http://www.math.gatech.edu/~thomas/FC/fourcolor.html.

  24. In the published version (Robertson et al. 1996, p. 17), the first sentence reads slightly different, without reference to the verification: “We began by trying to read the A&H proof, but very soon gave this up.”

  25. This is due to problems with the verification of the proof: “As part of the peer-review process, a panel of 12 referees appointed by the Annals of Mathematics studied the proof for four full years, finally returning with the verdict that they were ‘99 % certain’ of the correctness.” (Avigad and Harrison 2014, p. 69).

  26. At some places, also computer assistance was used; but in a much less extensive way than for the four colour theorem or the Kepler conjecture.

  27. “I have described the Classification as a theorem, and at this time I believe that to be true. Twenty years ago I would also have described the Classification as a theorem. On the other hand, ten years ago, while I often referred to the Classification as a theorem, I knew formally that that was not the case, since experts had by then become aware that a significant part of the proof had not been completely worked out and written down.” (Aschbacher 2004, p. 737f) and “After all, the probablity of an error in the proof is one.” (Aschbacher 2005, p. 2402).

  28. “[T]he utility of the theorem steems from two facts: [...]. Second, the explicit description of the groups on the list L supplied by very effective representations of most of the groups, make it possible to obtain a vast amount of detailed information about the groups.” (Aschbacher 2005, p. 2403f).

  29. Cited according to Hughes (1987, p. 65) where it is given as answer of Polya to the Hughes’s question: “What is proof?”

References

  • Alama J, Kahle R (2013) Checking proofs. In: Aberdein A, Dove IJ (eds) The argument of mathematics, volume 30 of logic, epistemology and the unity of science. Springer, Berlin, pp 147–170

    Google Scholar 

  • Aschbacher M (2004) The status of the classification of the finite simple groups. Not Am Math Soc 51(7):736–740

    Google Scholar 

  • Aschbacher M (2005) Highly complex proofs and implications of such proofs. Philos Trans R Soc A 363:2401–2406

    Article  Google Scholar 

  • Avigad J (2006) Mathematical method and proof. Synthese 153:105–149

    Article  Google Scholar 

  • Avigad J, Harrison J (2014) Formally verified mathematics. Commun ACM 57(4):66–75

    Article  Google Scholar 

  • Baaz M (1999) Note on the generalization of calculations. Theor Comput Sci 224(1–2):3–11

    Article  Google Scholar 

  • Baaz M, Pudlák P (1993) Kreisel’s conjecture for \(l\exists _1\). In: Clote P, Krajíček J (eds) Arithmetic proof theory and computational complexity. Oxford University Press, Oxford, pp 30–49

    Google Scholar 

  • Bourbaki N (1950) The architecture of mathematics. Am Math Mon 57(4):221–232

    Article  Google Scholar 

  • Dieudonné J (1985) Geschichte der Mathematik, 1700–1900. Vieweg, Berlin

  • Došen K, Petrić Z (2004) Proof-theoretical coherence. KCL Publications, London

    Google Scholar 

  • Ganesalingam M, Gowers WT (2013) A fully automatic problem solver with human-style output. CoRR, abs/1309.4501

  • Gray J (2013) Henri Poincaré. Princeton University Press, Princeton

    Google Scholar 

  • Hales TC (2014) Mathematics in the age of the Turing machine. In: Downey R (ed) Turing’s legacy: developments from Turing’s ideas in logic, volume 42 of lecture notes in logic. ASL and Cambridge University Press, pp 253–298

  • Hardy GH, Wright EM (1960) An introduction to the theory of numbers, 4th edn. Oxford University Press, Oxford

    Google Scholar 

  • Hughes B (1987) Mathematical proof: origins and development. In: Grattan-Guinness I (ed) History in mathematics education. Number 21 in Cahiers d’Histoire et de Philosophie des Sciences. Nouvelle Série, pp 65–72. Société Française d’Histoire des Sciences et des Techniques. Belin

  • Kahle R (2014) Towards the structure of mathematical proof. In: England M et al (eds) Joint proceedings of the MathUI, OpenMath and ThEdu workshops and work in progress track at CICM, vol 1186 of CEUR workshop proceedings

  • Krajíček J, Pudlák P (1988) The number of proof lines and the size of proofs in first order logic. Arch Math Log 27:69–84

    Article  Google Scholar 

  • Lambek J (1968) Deductive systems and categories. I: syntactic calculus and residuated categories. Math Syst Theory 2:287–318

    Article  Google Scholar 

  • Lambek J (1969) Deductive systems and categories II. Standard constructions and closed categories. In: Hilton P (ed) Category theory, homology theory and applications, volume 86 of lecture notes in mathematics, vol 86. Springer, pp 76–122

  • Lamport L (1995) How to write a proof. Am Math Mon 102(7):600–608

    Article  Google Scholar 

  • Lamport L (2012) How to write a 21st century proof. J Fixed Point Theory Appl 11:43–63

    Article  Google Scholar 

  • Leron U (1983) Structuring mathematical proofs. Am Math Mon 90(3):174–185

    Article  Google Scholar 

  • Loomis ES (1968) The Pythagorean proposition. Ann Arbor Michigan, 1968. Reprint of the 2nd edition from 1940. First published in 1927

  • Mancosu P (2000) On mathematical explanation. In: Grosholz E, Breger H (eds) The growth of mathematical knowledge. Kluwer, Netherlands, pp 103–119

    Chapter  Google Scholar 

  • Mancosu P (2001) Mathematical explanation: problems and prospects. Topoi 20:97–117

    Article  Google Scholar 

  • Necula GC (1997) Proof-carrying code. In: POPL ’97. ACM Press, pp 106–119

  • Prawitz D (1965) Natural deduction, a proof-theoretical study. Almquist and Wiksell, Stockholm

    Google Scholar 

  • Prawitz D (1971) Ideas and results in proof theory. In: Fenstad JE (ed) Proceedings of the Second Scandinavian Logic Symposium. North-Holland, pp 235–307

  • Robertson N, Sanders DP, Seymour PD, Thomas R (1996) A new proof of the four colour theorem. Electron Res Announc Am Math Soc 2:17–25

    Article  Google Scholar 

  • Scott D (2006) Foreword. In: Wiedijk F (ed) The seventeen provers of the world, volume 3600 of lecture notes in computer science. Springer, pp vii–xii

  • Steiner M (1978) Mathematical explanation. Philos Stud 34:133–151

    Article  Google Scholar 

  • Straßburger L (2005) What is a logic, and what is a proof? In: Beziau J-Y (ed) Logica Universalis. Birkhäuser, Basel, pp 135–145

    Chapter  Google Scholar 

  • Trybulec A (2006) Mizar. In: Wiedijk F (ed) The seventeen provers of the world, volume 3600 of lecture notes in computer science, vol 3600. Springer, pp 20–23

  • Wenzel M (1999) Isar—a generic interpretative approach to readable formal proof documents. In: Bertot Y, Dowek G, Hirschowitz A, Paulin C, Théry L (eds) Theorem proving in higher order logics, volume 1690 of lecture notes in computer science. Springer, pp 167–184

  • Wenzel M (2002) Isabelle/Isar—a versatile environment for human-readable formal proof documents. PhD thesis, Institut für Informatik, Technische Universität München

  • Wenzel M, Paulson L (2006) Isabelle/Isar. In: Wiedijk F (ed) The seventeen provers of the world, volume 3600 of lecture notes in computer science. Springer, pp 41–49

  • Wiedijk F (ed) (2006) The seventeen provers of the world, volume 3600 of lecture notes in computer science. Springer

Download references

Acknowledgments

Research supported by the Portuguese Science Foundation, FCT, through the projects Hilbert’s Legacy in the Philosophy of Mathematics, PTDC/FIL-FCI/109991/2009 and The Notion of Mathematical Proof, PTDC/MHC-FIL/5363/2012.

Author information

Authors and Affiliations

  1. CENTRIA, CMA, and DM, FCT, Universidade Nova de Lisboa, Caparica, 2829-516, Portugal

    Reinhard Kahle

Authors
  1. Reinhard Kahle
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Reinhard Kahle.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Kahle, R. What is a Proof?. Axiomathes 25, 79–91 (2015). https://doi.org/10.1007/s10516-014-9252-9

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10516-014-9252-9

Keywords

Search

Navigation