Reflections on Formalized Mathematics

John Harrison.

Unpublished draft, 23rd August 1995.

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 however, we do not offer polemics in support of such a project, but merely look at existing praxis and identify what we regard as the most interesting issues.

DVI or PostScript