“In my view, the choice between the conventional process by a human referee and computer verification is as evident as the choice between a sundial and an atomic clock in science.” – Tom Hales (from [4])

“The rapid advance of computers has helped dramatize this point, because computers and people are very different. For instance, when Appel and Haken completed a proof of the 4-color map theorem using a massive automatic computation, it evoked much controversy. I interpret the controversy as having little to do with doubt people had as to the veracity of the theorem or the correctness of the proof. Rather, it reflected a continuing desire for human understanding of a proof, in addition to knowledge that the theorem is true” – Bill Thurston (from [6])

A machine-checked proof is a proof written in a piece of software called a ‘proof assistant’ which ensures the proof complies with the ‘axioms of mathematics’ and the rules of logic. The question of the significance of computers in proving theorems can be polarizing (and for good reason). The quotations above represent some points of view relevant to this topic. In this post we will try answer three questions:

- What exactly is a computer-assisted proof?
- What are the advantages and the drawbacks of using computers to prove theorems?
- What should an interested person do to start learning to use proof assistants?

Continue reading “Machine-Checked Proof” »