@article{d6e29fac09df405ba8874e6a664eafeb,
title = "What is a proof?",
abstract = "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",
keywords = "mathematical proof, automated theorem proving , schematic proof, constructive omega rule",
author = "Alan Bundy and Mateja Jamnik and Andrew Fugard",
year = "2005",
month = "10",
doi = "10.1098/rsta.2005.1651",
language = "English",
volume = "363",
pages = "2377--2391",
journal = "Philosophical Transactions A: Mathematical, Physical and Engineering Sciences",
issn = "1364-503X",
publisher = "The Royal Society",
number = "1835",
}