John Harrison.
Unpublished draft, 23rd August 1995.
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 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.