Mathematical Structures in Computer Science

Paper

Zen and the art of formalisation

ANDREA ASPERTIa1 and JEREMY AVIGADa2

a1 Department of Computer Science, University of Bologna, Italy Email: asperti@cs.unibo.it

a2 Departments of Philosophy and Mathematical Sciences, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213, U.S.A. Email: avigad@cmu.edu

N. G. de Bruijn, now professor emeritus of the Eindhoven University of Technology, was a pioneer in the field of interactive theorem proving. From 1967 to the end of the 1970's, his work on the Automath system introduced the architecture that is common to most of today's proof assistants, and much of the basic technology. But de Bruijn was a mathematician first and foremost, as evidenced by the many mathematical notions and results that bear his name, among them de Bruijn sequences, de Bruijn graphs, the de Bruijn–Newman constant, and the de Bruijn–Erdös theorem. The quotation above is thus interesting not because it is a reflection on his expertise in formal verification, but, rather, of his convictions as a working mathematician.

(Received November 19 2010)

(Revised December 15 2010)

(Online publication July 01 2011)