N.G. de Bruijn was a well established mathematician before deciding in 1967 at the age of 49 to work on a new direction related to Automating Mathematics. In the 1960s he became fascinated by the new computer technology and decided to start the new Automath project where he could check, with the help of the computer, the correctness of books of mathematics. Through his work on Automath, de Bruijn started a revolution in using the computer for verification, and since, we have seen more and more proof-checking and theorem-proving systems.
Automath was written in Algol 60 and implemented on the primitive computers of the sixties. Thirty-five years on, both technology and theory have evolved a lot leading to impressive new directions in using the computer for manipulating and checking mathematics. This present volume is a collection of papers with a personal flavour. It consists of 11 articles which propose interesting variations to or examples of mechanising mathematics and illustrate different developments in symbolic computation in the past 35 years.
The first paper is by de Bruijn himself where he uses his experience of automating mathematics to reason about the human mind. Then, Barendregt proposes a mathematical proof language between informal and formalised mathematics which helps make proof assistants more user friendly. Then Constable explains how Automath's telescopes, books and definitions compare to recent developments in computational type theory made by his Nuprl group. Then Huet describes two design issues in symbolic computations and puts together convincingly two techniques which on the surface may seem unrelated: managing contexts and sharing. The article by Kamareddine, Laan and Nederpelt, studies the position of Automath within the framework of Pure Type Systems. The article of Franssen presents several ideas to design a Hoare Logic conforming to de Bruijn's criteria of a logic whose derivations are mechanically checked. The article of Arnon Avron argues that for automated reasoning, there is an interesting logic, somewhere strictly between first and second order logic, determined essentially by an analysis of transitive closure, yielding induction. The article of Randall Holmes presents a formal treatment and reports on an initial implementation of the ramified type theory used in Russell and Whitehead's Principia Mathematica. The paper of Ruiz-Reina etal, formalises and proves in the ACL2 theorem prover results concerning the multiset relation and other non-trivial mathematical theorems. The article of Gabbay presents a generalisation of Fraenkel-Mostowski (FM) set theory within higher-order logic, and applies it to model Milner's $\pi$-calculus. The article of Siekmann etal, presents a good overview and motivation of the $\Omega$mega system and discusses three different styles of proof development in $\Omega$mega using the example of the irrationality of $\sqrt 2$.