Automated deduction

AMS Notices

Formal Proof Issue (2008)

A Special Issue on Formal Proof. (Nov. 2008)

Using computers in proofs both extends mathematics with new results and creates new mathematical questions about the nature and technique of such proofs. This special issue features a collection of articles by practitioners and theorists of such formal proofs which explore both aspects.


(pp. 1363)
Formal Proof
Thomas Hales

(pp. 1370)
Formal Proof--The Four-Color Theorem
Georges Gonthier

(pp. 1382)
Formal Proof--Theory and Practice
John Harrison

(pp. 1395)
Formal Proof--Getting Started
Freek Wiedijk

Jeremy Avigad

Jeremy Avigad (home page at Carnegie Mellon) is “a professor in the Department of Philosophy and Department of Mathematical Sciences at Carnegie Mellon University, and Director of Graduate Studies in Philosophy.” He is also “associated with Carnegie Mellon's interdisciplinary program in Pure and Applied Logic.”

Avigad (2005)

Mathematical method and proof PDF

Jeremy Avigad (ude.umc|dagiva#ude.umc|dagiva)
Carnegie Mellon University

Abstract. On a traditional view, the primary role of a mathematical proof is to warrant the truth of the resulting theorem. This view fails to explain why it is very often the case that a new proof of a theorem is deemed important. Three case studies from elementary arithmetic show, informally, that there are many criteria by which ordinary proofs are valued. I argue that at least some of these criteria depend on the methods of inference the proofs employ, and that standard models of formal deduction are not well-equipped to support such evaluations. I discuss a model of proof that is used in the automated deduction community, and show that this model does better in that respect.

Avigad (2007)

Excerpt from “Jeremy Avigad's interview in Philosophy of Mathematics: 5 Questions, edited by Vincent F. Hendricks and Hannes Leitgeb. The book is released in December 2007 by Automatic Press / VIP.”

In 2004, I earned a measure of recognition from the formal verification community by verifying a proof of the prime number theorem, with the help of some students at Carnegie Mellon. Soon after, Georges Gonthier announced a verification of the four color theorem, and Thomas Hales announced a verification of the Jordan curve theorem. Hales has moreover launched an ambitious project to verify his proof of the Kepler conjecture, and Gonthier is currently overseeing a project to verify the Feit-Thompson theorem. Success in these endeavors requires, among other things, having the computer be able to verify straightforward mathematical inferences, without requiring the user to spell out the details. Getting computers to do so, in turn, requires a logical modeling and classification of the relevant inferences, and the development of procedures that can fill in the details automatically.

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License