file.pdf (148.74 kB)
Download file

Zen and the art of formalisation

Download (148.74 kB)
journal contribution
posted on 01.11.2010, 00:00 by Andrea Asperti, Jeremy AvigadJeremy Avigad

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.

History

Publisher Statement

Copyright © Cambridge University Press

Date

01/11/2010

Usage metrics

Categories

Keywords

Exports