Computer theorem proving in math

by Carlos Simpson

Abstract: We give an overview of issues surrounding computer-verified theorem proving in the standard pure-mathematical context. This is based on my talk at the PQR conference (Brussels, June 2003).

Version 1, submitted to the ccsd on November 15th, 2003:
dvi, ps , pdf , TeX source .

Here are links to the Coq proof files included invisibly in the TeX source:
groundwork7.v , notation9.v , order2.v (forming a unit)
qua.v
h1a.v
The revised version of February 20th, 2004, (tex, ps, pdf, dvi), is shortened to 29 pages but also has added references, such as a reference to L. Chicli's thesis, as well as the references and other remarks suggested by several readers (thanks go out to D. Grayson, J. Lipman, J. McKay, P. Rudnicki, J. Koch as well as the referee). One of the chapters has basically been removed. Also the Coq proof files are no longer bundled into the source file in the ccsd and Arxiv versions. Instead, these have been spun off into a separate preprint,
Set-theoretical mathematics in Coq (tex, ps, pdf, dvi), math.LO/0402336.
See the index file for the proof files (which are part of the tar archive for the source in the Arxiv version).
The revised version of April 8th, 2004 (tex, ps, pdf, dvi) takes into account further important remarks by the referee concerning the history of the subject, and adds several references.