- Abstract:
-
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
- @Article{EDI-INF-RR-0394,
- 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 = {http://www.journals.royalsoc.ac.uk/(cr2nhhfjbaokdcfggliy3pqg)/app/home/issue.asp?referrer=parent&backto=journal,2,115;linkingpublicationresults,1:102021,1},
- }
|
