Computer theorem proving in math
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:
TeX source .
Here are links to the Coq proof files included invisibly in the
order2.v (forming a unit)
The revised version of February 20th, 2004,
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
index file for the proof files (which are part of the tar archive for the source in the
The revised version of April 8th, 2004
takes into account further important remarks by the referee concerning the history
of the subject, and adds several references.