Hostname: page-component-7c8c6479df-94d59 Total loading time: 0 Render date: 2024-03-29T10:57:39.523Z Has data issue: false hasContentIssue false

Zen and the art of formalisation

Published online by Cambridge University Press:  01 July 2011

ANDREA ASPERTI
Affiliation:
Department of Computer Science, University of Bologna, Italy Email: asperti@cs.unibo.it
JEREMY AVIGAD
Affiliation:
Departments of Philosophy and Mathematical Sciences, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213, U.S.A. Email: avigad@cmu.edu

Extract

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.

Type
Paper
Copyright
Copyright © Cambridge University Press 2011

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)