Introduction

Abstract

The chapter starts with quick glimpses of some major steps in the history of the formalization of mathematical reasoning: Aristotle’s syllogisms, Leibniz’s program, Boole’s algebra of propositions, Frege’s Begriffsschrift, Peano’s axiomatization of arithmetic, Whitehead and Russell’s attempt at formalizing the whole corpus of mathematics, Descartes’ reduction of geometry to algebra, Cauchy’s formalization of continuity, Dedekind’s definition of the system of real numbers, Cantor’s transfinite set theory, Russel’s paradox, Zermelo–Fraenkel’s axiomatization of set theory, Hilbert’s program, Gödel’s negative results, etc.

Proof verifiers are then introduced. It is argued that to ease interaction with humans, they must be equipped with some degree of mathematical intelligence, in the form of deduction mechanisms. The main such mechanisms implemented in the proof-verification system Ref, developed by the authors, are quickly reviewed, as well as the most important ingredients of its formalism. Among them, set theory and ‘theory’-based reasoning play a preeminent role.

Finally, a survey of the major sequence of definitions and proofs considered in the text is provided, leading from the barest rudiments of set theory to the formulation of a special form of the Cauchy integral theorem.