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

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.