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.