||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.