FOM: Re: 107:Automated Proof Checking

[Roger Bishop Jones]

In relation to Harvey's note on automated proof
checking there is of course a vast literature from
research programmes extending back through about
four decades.

Mizar, which he mentions, is possibly the system which
has been most concerned to make proofs readable
to mathematicians, and it would therefore be of
interest to know more about Harvey's reasons for
thinking that his proposal would improve on Mizar.

However, my reason for posting is to refer readers
interested in but not familiar with this topic to
a relevant paper by John Harrison.

His paper, entitled "Formalising Mathematics" is online
as html at:
 http://www.rbjones.com/rbjpub/logic/jrh0100.htm
or in postscript at:
 http://www.cl.cam.ac.uk/users/jrh/papers/form-math3-cm.ps.gz
and is a broad discussion of the topic covering
history, philosophy, theory, and pragmatics.

John has written much of relevance to this topic, including
his doctoral dissertation "Theorem Proving with the Real Numbers"
which is concerned with the formalisation of real analysis,
and has been published by Springer in their
distinguished dissertation series.

For a full list of his writings see:
 http://www.cl.cam.ac.uk/users/jrh/papers.html

Roger Jones