Automath

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

Automath was the first working system for checking mathematics by computer. N. G. de Bruijn designed it at Eindhoven in the late 1960s, and his group used it through the 1970s. This page states what the project set out to do, what its languages were, what its largest text showed, and which of its ideas Lean still uses.

A language for whole books

De Bruijn's own survey of 1980 says the project "was conceived in 1966" and that the first report was written in 1968. His preface to van Benthem Jutting's book of 1979 gives early 1967 instead, and the Automath Archive at Eindhoven dates the first ideas to around 1967 and the large-scale work to roughly 1970–1975. An early published account is de Bruijn's paper to the Symposium on Automatic Demonstration at Versailles in December 1968, printed in 1970, which says that the language was developed in 1967 and 1968.

The aim was a way of writing entire mathematical theories so precisely that their correctness could be checked by formal operations on the text, without any appeal to meaning. If the checking is formal, a computer can do it. The name means mathematics aided by an automaton.

An Automath text is a book: a sequence of lines, each checked against the lines before it. A line either opens an assumption (a variable of a stated type), makes a definition (a name for an expression of a stated type), or introduces a primitive notion, which is how axioms enter. A theorem is a definition whose type is the proposition and whose body is the proof. Contexts are named by their last variable, so a later line can return to an earlier context without repeating it.

Propositions as types

Automath treated a proof of a proposition as an object whose type is that proposition. De Bruijn's survey traces this idea to Curry and Feys (1958) and to Howard (1969), and states that it appeared in his own 1968 work independently of them. In the same survey he records the name proof irrelevance for the rule that any two proofs of one proposition are definitionally equal, introduced in a report of 1974. Both ideas are part of Lean's logic: see Propositions as types and Proof irrelevance and subsingleton elimination.

The languages

Automath was a family of languages, not one. The survey presents them in stages. A simple base language, PAL, admits typed variables and definitions; adding lambda abstraction gives AUT-68, long called simply Automath; a slightly stronger variant is AUT-QE. J. Zucker's AUT-PI extended AUT-68 in another direction and was easier to write. AUT-SL ("single line") removed the restrictions on abstraction so that a whole book could be written as one expression, mainly to give the theory a clean form. AUT-68 and AUT-QE were the languages most used.

The survey reports that for these languages checking is decidable: a machine can always settle whether a line is correct. Doing so efficiently was harder, since the naive method of reducing expressions to normal form could repeat a great deal of work. Most of the work on the checking programs was done by I. Zandleven between 1971 and 1976.

Landau's Grundlagen

The test of the system was a whole textbook. L. S. van Benthem Jutting translated Edmund Landau's Grundlagen der Analysis (1930), which constructs the number systems from the natural numbers up to the complex numbers, line by line into AUT-QE. A five-volume report of the translation appeared in 1976, and his experiences are in his doctoral thesis, written under de Bruijn and W. Peremans and completed at Eindhoven in 1977. The thesis was published in 1979 as Mathematical Centre Tracts 83.

De Bruijn explained the choice of book: Landau's steps do not grow larger towards the end, and the group wanted to show that Automath could handle mathematics written without it in mind, rather than mathematics rewritten to suit it.

The files outlived the machines. By the early 1990s the original checkers no longer ran, because the language they were written in and the computer they ran on no longer existed, and the copies of the translation had become corrupted. Freek Wiedijk repaired them from the printed 1976 report and wrote a new checker for AUT-68 and AUT-QE. By his count the translation has 10,702 lines and is about 3.9 times the size of the German original, or 3.7 times when both files are compressed; he had earlier named that compressed ratio the de Bruijn factor. He reports that the two checkers of the 1970s took about 35 and 69 minutes over it, and his own 0.6 seconds on a 1 GHz machine.

What it did not have

Automath had no automation. Every proof term was written by hand, and the checker only confirmed it. It had no inductive types, so basic types had to be introduced by axioms; and the large texts of the 1970s used classical logic. Wiedijk writes that the project was very active in the 1970s and ended when its funding stopped.

What lasted

De Bruijn indices. In 1972 de Bruijn proposed writing a bound variable not by a name but by a number counting how many binders lie between the variable and the one that binds it. Renaming bound variables causes considerable trouble in programs that manipulate formulas, and with this notation it never arises. The paper claims that its notation is good for machines and for reasoning about the calculus, but not that it is easy for human readers, and a section of it applies the notation to Automath. Lean represents a bound variable in exactly this way: in its type of expressions, the constructor for a bound variable carries a de Bruijn index.

The de Bruijn criterion. A proof may run to megabytes, yet the program that checks it can be small enough for a person to inspect. Barendregt and Wiedijk call a system that allows its proofs to be checked independently by such a small program one that satisfies the de Bruijn criterion. The name is later than Automath; the practice it names is Automath's. Lean's version of it is described at The small trusted core and Proof export and independent checkers.

The line to the Calculus of Constructions. Geuvers and Nederpelt state that Automath's goals and syntactic ideas inspired Thierry Coquand and Gérard Huet to develop the Calculus of Constructions, the ancestor of the logic Lean uses. That line is followed at The Calculus of Constructions.

The standard collection of the project's papers, including parts of van Benthem Jutting's thesis and de Bruijn's survey, is Selected Papers on Automath (1994).

Provenance: de Bruijn's 1980 survey, Wiedijk's 2002 paper, Barendregt and Wiedijk's 2005 paper and Geuvers and Nederpelt's 2022 paper were read for this page; the 1970 and 1972 papers were read in their opening pages only, in scans. The published form of van Benthem Jutting's thesis was read in its title page, contents, de Bruijn's preface and introduction. The 1994 collection was not opened; its details come from the publisher's record.

Next

LCF and the tactic idea