Edited by Jordan Bohall (University of Illinois, Urbana-Champaign)
|Summary||Computer proofs are those proofs in mathematics that have been at least partially and, sometimes, completely proven by computer. The landmark Appel and Haken proof of the Four Color Theorem in 1976 used a large scale exhaustion-style proof method carried out partially by computer. Shortly before the Appel-Haken proof and up to the present, computer proofs have proven useful both in pure mathematics and areas such as artificial intelligence and machine learning. However, the proof-by-exhaustion methods are contentious in that they represent deductions which are not surveyable by humans in a reasonable amount of time. So, questions for computer proof involve what counts as mathematical proof, are empirical methodologies acceptable in pure mathematics, and do we have certainty that the theorem, etc. proven by computer are indeed proven.|
|Key works||Tymoczko 1979, Burge 1998, Manders 1989|
Using PhilPapers from home?
Create an account to enable off-campus access through your institution's proxy server.
Monitor this page
Be alerted of all new items appearing on this page. Choose how you want to monitor it:
David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers