About Automath

Automath is a language designed by N.G. the Bruijn (1918-2012) in the late sixties in order to represent mathematical proofs in the computer.

The ideas of Automath started around 1967 and gave rise to a large-scale project (roughly 1970-1975). It was the first big enterprise for automated verification of mathematics. The system was tested by treating a full text book (E. Landau's 'Grundlagen der Analysis'), which could be accomplished succesfully in spite of computer power limitations and in spite of almost complete lack of software support and text editing facilities. Below you can find two articles that can serve as an introduction to the Automath project.

A general description of the various aspects of the spirit of the Automath project was presented in the section "Computers and Mathematics" (edited by Jon Barwise) of the Notices of the American Mathematical Society (Jan. 1991, volume 38, number 1, pages 8-15) under the title "Checking Mathematics with Computer Assistance". It is reproduced here.

Also available are sheets (PDF file) of a 2003 lecture of prof. de Bruijn, recollecting the Automath project.

Click here for a list of writing by prof. N.G. de Bruijn on Automath and related subjects.

N.G. De Bruijn died in February 2012, at the age of 93 years. In his honour, Rob Nederpelt and Francien Dechesne wrote an article on De Bruijn's road from his mathematical practice to the Automath project, which has been published in the Mathematical Intelligencer, Volume 34, Issue 4 , pp 4-11. The Nieuw Archief voor Wiskunde dedicated most of the March 2013 issue to the work of N.G. De Bruijn, with commemorative contributions by J.W. Klop, Guido Janssen, Pieter Moree, Nico Temme, Ton Kloks and Rob Tijdeman, Roel de Vrijer, and Henk Barendregt (in Dutch).