Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:The Nature of Mathematical Proof
Authors: Alan Bundy ; Michael Atiyah ; Angus Macintyre ; Donald Mackenzie
Date:Oct 2005
Publication Title:Philosophical Transactions of the Royal Society A
Publication Type:Journal Article Publication Status:Published
Volume No:363(1835) Page Nos:2461-
Mathematical proof is one of the highest intellectual achievements of humankind. It contains the deepest, most complex and most rigorous arguments of which we are capable. Until the last half century, mathematical proof was the exclusive preserve of human mathematicians. However, following the logical formalisation of proof and the invention of electronic computers, it has become possible to automate the process of proof. Initially, automatic theorem proving computer programs were only capable of proving trivial theorems. But with the exponentially increasing speed and storage capacity of computers, and the development of more sophisticated theorem-proving software, it has now become possible to prove open conjectures by mechanical means. These developments have raised questions about the nature of mathematical proof. Some have argued that mathematical proof is an essentially social process in which humans interact and convince each other of the correctness of their arguments. Not only are computer 'proofs' are hard for humans to understand but computers are unable to take part in this social process, so it is argued that whatever theorem-proving computers do it is not really Mathematics. Some proofs, such as the Four Colour Theorem and Kepler's Conjecture, have required essential computer assistance to check a large number of Cases. Because this computer processing is inaccessible to human mathematicians, many of them have refused to accept these part-mechanical proofs. On the other hand, computer scientists routinely use mechanical proof for the formal verification of the correctness of their computer programs. They argue that these verification proofs are so long and complicated, and humans so error prone, that only a completely computer-checked proof merits the level of confidence required for a safety- or security-critical application. Also, some mathematicians have found computer systems to be a useful experimental tool, whi
Links To Paper
This is the Royal Society web page from which the special journal issue can be purchased.
2nd Link
Bibtex format
author = { Alan Bundy and Michael Atiyah and Angus Macintyre and Donald Mackenzie },
title = {The Nature of Mathematical Proof},
journal = {Philosophical Transactions of the Royal Society A},
year = 2005,
month = {Oct},
volume = {363(1835)},
pages = {2461-},
url = {,2,115;linkingpublicationresults,1:102021,1},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh