N.G. de Bruijn’s contribution to the formalization of mathematics

Research output: Contribution to journalArticleAcademicpeer-review

1 Citation (Scopus)


N.G. (Dick) de Bruijn was the first to develop a formal language suitable for the complete expression of a mathematical subject matter. His formalization does not only regard the usual mathematical expressions, but also all sorts of meta-notions such as definitions, substitutions, theorems and even complete proofs. He envisaged (and demonstrated) that a full formalization enables one to check proofs automatically by means of a computer program. He started developing his ideas about a suitable formal language for mathematics in the end of the 1960s, when computers were still in their infancy. De Bruijn was ahead of his time and much of his work only became known to a wider audience much later. In the present paper we highlight de Bruijn’s contributions to the formalization of mathematics, directed towards verification by a computer, by placing these in their time and by relating them to parallel and later developments. We aim to explain some of the more technical aspects of de Bruijn’s work to a wider audience of interested mathematicians and computer scientists. Keywords: Type theory; Formalizing mathematics; Lambda calculus; Proof assistants
Original languageEnglish
Pages (from-to)1034-1049
Number of pages16
JournalIndagationes Mathematicae. New Series
Issue number4
Publication statusPublished - 2013


Dive into the research topics of 'N.G. de Bruijn’s contribution to the formalization of mathematics'. Together they form a unique fingerprint.

Cite this