[FOM] Computer theorem proving in math

[Michael Thayer]

After some recent discussions on this topic, some members might be interested in the following paper:


math.HO/0311260 [<http://xxx.lanl.gov/abs/math.HO/0311260>abs, <http://xxx.lanl.gov/ps/math.HO/0311260>ps, <http://xxx.lanl.gov/pdf/math.HO/0311260>pdf, <http://xxx.lanl.gov/format/math.HO/0311260>other] :

Title: Computer theorem proving in math
Authors: <http://xxx.lanl.gov/find/math/1/au:+Simpson_C/0/1/0/all/0/1>Carlos T. Simpson
Subj-class: History and Overview; Category Theory; Algebraic Geometry; Differential Geometry; Logic

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). 




http://xxx.lanl.gov/abs/math.HO/0311260