TY - JOUR
T1 - What is a proof?
AU - Bundy, Alan
AU - Jamnik, Mateja
AU - Fugard, Andrew
PY - 2005/10
Y1 - 2005/10
N2 - To those brought up in a logic-based tradition there seems to be a simple and clear definition of proof. But this is largely a 20th century invention; many earlier proofs had a different nature. We will look particularly at the faulty proof of Euler's Theorem and Lakatos' rational reconstruction of the history of this proof. We will ask: how is it possible for the errors in a faulty proof to remain undetected for several years - even when counter-examples to it are known? How is it possible to have a proof about concepts that are only partially de ned? And can we give a logic-based account of such phenomena? We introduce the concept of schematic proofs and argue that they over a possible cognitive model for the human construction of proofs in mathematics. In particular
AB - To those brought up in a logic-based tradition there seems to be a simple and clear definition of proof. But this is largely a 20th century invention; many earlier proofs had a different nature. We will look particularly at the faulty proof of Euler's Theorem and Lakatos' rational reconstruction of the history of this proof. We will ask: how is it possible for the errors in a faulty proof to remain undetected for several years - even when counter-examples to it are known? How is it possible to have a proof about concepts that are only partially de ned? And can we give a logic-based account of such phenomena? We introduce the concept of schematic proofs and argue that they over a possible cognitive model for the human construction of proofs in mathematics. In particular
KW - mathematical proof
KW - automated theorem proving
KW - schematic proof
KW - constructive omega rule
U2 - 10.1098/rsta.2005.1651
DO - 10.1098/rsta.2005.1651
M3 - Article
VL - 363
SP - 2377
EP - 2391
JO - Philosophical Transactions A: Mathematical, Physical and Engineering Sciences
JF - Philosophical Transactions A: Mathematical, Physical and Engineering Sciences
SN - 1364-503X
IS - 1835
ER -