Projects per year
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 logicbased 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 VE+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 logicbased account of schematic proofs, distinguishing them from Hilbertian proofs, and showing why they are error prone.
Original language  English 

Title of host publication  Proof Technology in Mathematics Research and Teaching 
Publisher  SpringerVerlag GmbH 
Pages  5971 
Number of pages  11 
ISBN (Electronic)  9783030284831 
ISBN (Print)  9783030284824 
DOIs  
Publication status  Published  28 Oct 2019 
Publication series
Name  Mathematics Education in the Digital Era 

Publisher  Springer 
Volume  14 
ISSN (Print)  22118136 
Fingerprint
Dive into the research topics of 'A Common Type of Rigorous Proof that Resists Hilbert’s Programme'. Together they form a unique fingerprint.Projects
 3 Finished

The integration and interaction of multiple mathematical Reasoning Processes
Bundy, A., Aspinall, D., Colton, S., Fleuriot, J., Gow, J., Grov, G., Ireland, A., Jackson, P., Mcneill, F., Michaelson, G. & Smaill, A.
1/11/15 → 31/10/19
Project: Research

AUTOMATED DISCOVERY OF MATHEMATICS
Bundy, A., Colton, S. & Smith, P.
1/08/03 → 31/08/06
Project: Research

The integration and interaction of multiple mathematical reasoning processes
Bundy, A., Dennis, L., Fleuriot, J., Ireland, A., Jackson, P., Richardson, J. & Smaill, A.
1/10/02 → 30/09/06
Project: Research