Welcome to The Automath Archive

The Automath Archive was created by the Brouwer Institute in Nijmegen and the Formal Methods section of Eindhoven University of Technology. Started by prof. H. Barendregt, in cooperation with Rob Nederpelt, this archive project was launched to digitize valuable historical articles and other documentation concerning the Automath project.

Initiated by prof. N.G. de Bruijn, the project Automath (1967 until the early 80's) aimed at designing a language for expressing complete mathematical theories in such a way that a computer can verify the correctness. This project can be seen as the predecessor of type theoretical proof assistants such as the well known Nuprl and Coq.

Prof. N.G. de Bruijn (1918-2012)

In 1994 a compilation of a number of papers about Automath appeared in 'Selected Papers on Automath', which now is the standard reference about the subject. While some of the articles related to the Automath project are published elsewhere, many interesting other parts of the documentation remained unavailable to the scientific world.

In honour of prof. N.G. de Bruijn's 85th birthday in 2003, we started to investigate the paper archive of the Automath project that is still present at Eindhoven University, and to digitize a number of articles and other documentation. As a result, they are now available here, in this online archive.

We aim to make these documents, deposited by the Eindhoven University of Technology, accessible via the internet. For the first time one can access almost 200 documents related to the Automath project.