John Harrison.
Unpublished draft, 22nd February 1996.
NB! This paper is superseded by a
newer version
Abstract:
It is generally accepted that in principle it's possible to formalize
completely almost all of present-day mathematics. The practicability of
actually doing so is widely doubted, as is the value of the result. But
in the computer age we believe that such formalization is possible and
desirable. In contrast to the QED Manifesto (Anonymous 1994) however, we do not
offer polemics in support of such a project. We merely try to place the
formalization of mathematics in its historical perspective, as well as looking
at existing praxis and identifying what we regard as the most interesting
issues, theoretical and practical.
The Times versions are recommended for printing, but the Computer Modern
ones sometimes look better on previewers.
There is also a browsable version of the paper in HTML format;
thanks to Roger
Jones for this translation. This was published electronically in
volume 2 of
Mathesis Universalis, edited by Witold
Marciszewski.