Automath: a language in which a machine checks mathematics
In November 1968 N. G. de Bruijn issued a report at the Technological University Eindhoven on Automath, a language for writing mathematics in enough detail that a computer can check whether the text is correct. Such a text need not be the proof of a single theorem; it can hold an entire theory together with its rules of inference.
Why it matters
Instead of searching for a proof, the machine now checked a proof written by a person, line by line. This is the other half of machine proof, and later checking systems stand on it, among them the calculus of constructions, whose authors say its terms are inspired by the Automath formalisms.
According to the report, Automath is not a programming language: every text written according to its rules is claimed to correspond to correct mathematics. The checking processors were programmed in ALGOL; the author thanks L. S. van Benthem Jutting and L. G. F. C. van Bree. The report says the computer should never believe an incorrect line, and that the processor running in November 1968 needed no hints, though experience was still very limited. The report gives no figures. The first large check came later and is described in van Benthem Jutting's thesis, defended on 1 March 1977: a translation of Landau's Grundlagen der Analysis, about 500 pages, was verified on a Burroughs B6700 in Eindhoven, its last page in September 1975 and the whole book in a final run on 18 October 1975. The run took 2 hours, 42 minutes of it verification: 13,433 lines, 215,138 expressions, 2,519.7 seconds of checking. What the record does not claim: how many of Landau's theorems were checked; the thesis gives no such number.