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.