PMA Publisher: Published from the Principia Machina source

2026-10-15T19:35:23Z

Published from the Principia Machina source

← Older revision		Revision as of 19:35, 15 October 2026
Line 1:		Line 1:
	{{DISPLAYTITLE:Automath}}		{{DISPLAYTITLE:Automath}}
			{{Lean theorem prover map}}
	Automath was the first working system for checking mathematics by computer.<ref name="gn2022" /> 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.		Automath was the first working system for checking mathematics by computer.<ref name="gn2022" /> 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.

PMA Publisher: Published from the Principia Machina source

2026-10-14T18:01:11Z

Published from the Principia Machina source

New page

{{DISPLAYTITLE:Automath}}
Automath was the first working system for checking mathematics by computer.<ref name="gn2022" /> 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.<ref name="survey">N. G. de Bruijn, "A survey of the project Automath", in J. P. Seldin and J. R. Hindley (eds.), ''To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism'', Academic Press, 1980, pp. 579–606; reprinted in Nederpelt, Geuvers and de Vrijer (eds.), ''Selected Papers on Automath'' (1994), pp. 141–161. Scan in the Automath Archive: https://automath.win.tue.nl/archive/pdf/aut072.pdf</ref> 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.<ref name="cwi" /><ref name="archive">The Automath Archive, Eindhoven University of Technology, "About Automath". https://automath.win.tue.nl/aboutautomath.htm</ref> 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.<ref name="aut1970">N. G. de Bruijn, "The mathematical language AUTOMATH, its usage, and some of its extensions", in ''Symposium on Automatic Demonstration'', Lecture Notes in Mathematics 125, Springer, 1970, pp. 29–61. doi:10.1007/BFb0060623. Scan in the Automath Archive: https://automath.win.tue.nl/archive/pdf/aut002.pdf</ref>

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.<ref name="survey" /> The name means mathematics aided by an automaton.<ref name="gn2022">Herman Geuvers and Rob Nederpelt, "Characteristics of de Bruijn's early proof checker Automath", ''Fundamenta Informaticae'' 185 (4), 2022, pp. 313–336. doi:10.3233/FI-222112. Preprint: https://arxiv.org/abs/2203.01173</ref>

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.<ref name="gn2022" />

== 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.<ref name="survey" /> 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.<ref name="survey" /> Both ideas are part of Lean's logic: see [[Lean theorem prover/Explainers/Propositions as types|Propositions as types]] and [[Lean theorem prover/Foundations/Proof irrelevance and subsingleton elimination|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.<ref name="survey" /> AUT-68 and AUT-QE were the languages most used.<ref name="gn2022" />

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.<ref name="survey" />

== 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.<ref name="survey" /><ref name="wiedijk2002" /><ref name="mgp">Mathematics Genealogy Project, entry for Lambert S. van Benthem Jutting: Ph.D., Technische Universiteit Eindhoven, 1977, dissertation "Checking Landau's 'Grundlagen' in the Automath System", advisors N. G. de Bruijn and W. Peremans. https://www.mathgenealogy.org/id.php?id=63580</ref> The thesis was published in 1979 as Mathematical Centre Tracts 83.<ref name="cwi">L. S. van Benthem Jutting, ''Checking Landau's "Grundlagen" in the Automath System'', Mathematical Centre Tracts 83, Mathematisch Centrum, Amsterdam, 1979. ISBN 90-6196-147-5. Record and scan: https://ir.cwi.nl/pub/13104</ref>

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.<ref name="survey" />

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.<ref name="wiedijk2002">Freek Wiedijk, "A new implementation of Automath", ''Journal of Automated Reasoning'' 29 (3–4), 2002, pp. 365–387. doi:10.1023/A:1021983302516. Author's copy: https://www.cs.ru.nl/~freek/aut/aut.pdf</ref>

== What it did not have ==

Automath had no automation. Every proof term was written by hand, and the checker only confirmed it.<ref name="bw2005">Henk Barendregt and Freek Wiedijk, "The challenge of computer mathematics", ''Philosophical Transactions of the Royal Society A'' 363 (1835), 2005, pp. 2351–2375. doi:10.1098/rsta.2005.1650. Author's copy: https://www.cs.ru.nl/~freek/pubs/rspaper.pdf</ref> It had no inductive types, so basic types had to be introduced by axioms; and the large texts of the 1970s used classical logic.<ref name="wiedijk-page">Freek Wiedijk, "Automath" (notes accompanying the aut checker). https://www.cs.ru.nl/~freek/aut/</ref> Wiedijk writes that the project was very active in the 1970s and ended when its funding stopped.<ref name="wiedijk2002" />

== 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.<ref name="nameless">N. G. de Bruijn, "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem", ''Indagationes Mathematicae'' 34 (= ''Proceedings KNAW'' A 75), 1972, pp. 381–392. doi:10.1016/1385-7258(72)90034-0. Reprint from ''Selected Papers on Automath'' in the Eindhoven repository: https://alexandria.tue.nl/repository/freearticles/597619.pdf</ref> 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.<ref name="leanexpr">Lean 4 source, <code>src/Lean/Expr.lean</code>, documentation of <code>Expr.bvar</code>, version 4.34.1. https://github.com/leanprover/lean4/blob/v4.34.1/src/Lean/Expr.lean</ref>

'''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'''.<ref name="bw2005" /> The name is later than Automath; the practice it names is Automath's. Lean's version of it is described at [[Lean theorem prover/Explainers/The small trusted core|The small trusted core]] and [[Lean theorem prover/System/Proof export and independent checkers|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.<ref name="gn2022" /> That line is followed at [[Lean theorem prover/History/The Calculus of Constructions|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).<ref name="sp1994">R. P. Nederpelt, J. H. Geuvers and R. C. de Vrijer (eds.), ''Selected Papers on Automath'', Studies in Logic and the Foundations of Mathematics 133, North-Holland, Amsterdam, 1994. ISBN 0-444-89822-0. Publisher's page with contents: https://shop.elsevier.com/books/selected-papers-on-automath/nederpelt/978-0-444-89822-7</ref>

<blockquote>
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.
</blockquote>

== Next ==

[[Lean theorem prover/History/LCF and the tactic idea|LCF and the tactic idea]]

== References ==
<references />

Lean theorem prover/History/Automath - Revision history

PMA Publisher: Published from the Principia Machina source

PMA Publisher: Published from the Principia Machina source