Formalized Mathematics

Technical Report 36, Turku Centre for Computer Science (TUCS)

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. 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)

PostScript (Times font)

PostScript (CM font)

The Times versions are recommended for printing, but the Computer Modern ones sometimes look better on previewers. There is also an HTML version of this paper; thanks to Roger Jones for this translation. An earlier version of this was published electronically in volume 2 of Mathesis Universalis, edited by Witold Marciszewski.

Bibtex entry:

@TECHREPORT{harrison-form,
        author          = "John Harrison",
        title           = "Formalized Mathematics",
        institution     = "Turku Centre for Computer Science (TUCS)",
        address         = "Lemmink{\"a}isenkatu 14 A, FIN-20520 Turku,
                           Finland",
        year            = 1996,
        type            = "Technical Report",
        number          = 36,
        note            = "Available on the Web as
 {\verb+http://www.cl.cam.ac.uk/~jrh13/papers/form-math3.html+}"}