Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Reflections on Formalized Mathematics
Reflections on Formalized Mathematics
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.