Pure Mathematics in a Mechanized Logic

: 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. 1 Introduction The idea of reducing reasoning to computation in some kind of mechanical calculus is quite an old one. For example, Hobbes [1] remarked that `reasoning . . . is but reckoning', and even noted the difficulty of ensuring that logical reasoning is correct: For as Arithmeticians teach to adde and subtract in numbers [...] The Logicians te..