Formalized Mathematics

John Harrison.

Unpublished draft, 22nd February 1996.

NB! This paper is superseded by a newer version


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.

DVI (Times font) or PostScript (Times font) or PostScript (CM font)

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.