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.
The talk will accentuate the fact that the ideas of Automath arose independently of the worlds of logic and computer science (the latter hardly existed at the time). All of it was the effect of the immaculate precision of the language of mathematics that had reached such a high standard in the first half of the twentieth century.