Pure Mathematics in a Mechanized Logic

John Harrison.

Proceedings of the Finnish Artificial Intelligence Society (FAIS) symposium Logic, Mathematics and the Computer: History, Foundations and Applications, University of Helsinki, Metsätalo, 3-4 June 1996, pp. 153-169.

NB! Most of the contents of this paper are discussed in greater depth in my PhD thesis

Abstract:

It is widely believed that in principle it's possible to reduce most of present-day mathematics to reasoning in a formal logical system. The technical difficulty of actually doing so is quite formidable. However, the arrival of the computer is changing this situation, since computers are good at helping with such tedious symbolic manipulation. The computer formalization of mathematics is now a popular research topic. Here we report on our own development of mathematical analysis starting just from the axioms of simple type theory and reducing all reasoning (with the aid of the computer) to a formal deductive calculus of great simplicity.

DVI or PostScript

Bibtex entry:

@INPROCEEDINGS{harrison-fais,
        author          = "John Harrison",
        title           = "Pure Mathematics in a Mechanized Logic",
        booktitle       = "Proceedings of the Finnish Artificial Intelligence
                           Society Symposium: Logic, Mathematics and the
                           Computer",
        editor          = "Christoffer Gefwert and Pekka Orponen and
                           Juoko Sepp{\"a}nen",
        publisher       = "Finnish Artificial Intelligence Society",
        series          = "Suomen Teko{\"a}lyseuran julkaisuja",
        volume          = 14,
        year            = 1996,
        pages           = "153--169"}