A Common Type of Rigorous Proof that Resists Hilbert’s Programme

Alan Bundy, Mateja Jamnik

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

Abstract / Description of output

Following Hilbert, there seems to be a simple and clear definition of mathematical proof: it is a sequence of formulae each of which is either an axiom or follows from earlier formulae by a rule of inference. Automated theorem provers are based on this Hilbertian concept of proof, in which the formulae and rules of inference are represented in a formal logic. These logic-based proofs are typically an order of magnitude longer than the rigorous proofs produced by human mathematicians. There is a consensus, however, that rigorous proofs could, in principle, be unpacked into logical proofs, but this programme is rarely carried out because it would be tedious and uninformative. We argue that, for at least one class of rigorous proofs, which we will call 'schematic proofs', such a simple unpacking is not available. We will illustrate schematic proofs by analysing Cauchy's faulty proof of Euler's Theorem V-E+F = 2, as reported in \akatos's "Proofs and Refutaionts", and giving further examples from Nelsen's "Proofs with Words". We will then give a logic-based account of schematic proofs, distinguishing them from Hilbertian proofs, and showing why they are error prone.
Original languageEnglish
Title of host publicationProof Technology in Mathematics Research and Teaching
PublisherSpringer-Verlag GmbH
Number of pages11
ISBN (Electronic)978-3-030-28483-1
ISBN (Print)978-3-030-28482-4
Publication statusPublished - 28 Oct 2019

Publication series

NameMathematics Education in the Digital Era
ISSN (Print)2211-8136


Dive into the research topics of 'A Common Type of Rigorous Proof that Resists Hilbert’s Programme'. Together they form a unique fingerprint.

Cite this