Automath is a language designed by N.G. the Bruijn in the late sixties in order to represent mathematical proof in the computer. It's the direct ancestor of the "type theoretical" line of proof assistants from which the better known current ones are Nuprl and Coq.

This web page is the home of a modern reimplementation of Automath by Freek Wiedijk. It presents a portable, simple and fast checker (which is written in C) for the AUT-68 and AUT-QE languages.

The current version of the program is version 4.2. But because the manual describes version 4.1, that one is here too (although it hardly differs from the latest version: the main difference being that the new version can compile a Automath text to a "single line" representation.) Both are gzipped tar files containing a bunch of C files. Compile them all together and you have a program that reads Automath from its input and prints diagnostics about it to its output.

There's not enough documentation about this Automath implementation: for instance there's no Unix-style man page yet. All that currently exists is a short paper called A Nice and Accurate Checker for the Mathematical Language Automath (clicking this link will download a postscript file; there is a PDF version too) which contains the manual of version 4.1 of the system.

The largest Automath text that was written in the seventies was Jutting's translation of Landau's Grundlagen der Analysis (this link gives a gzipped tar file with both a plain TeX version of Landau's book as well as Jutting's translation.)

There are three main differences between Automath and the "modern" systems that have been derived from it:

• In the modern systems a proof object is generated by the user interactively invoking so-called "tactics". In Automath all proof terms have to be "coded" by hand. This means that Automath has no automation, but that on the other hand in Automath proofs are more explicit. (The Half system is an interesting attempt to compromise between these two worlds.)

• Automath has no "inductive types". This means that the basic types that in the modern systems are built from inductive types have to be introduced axiomatically in Automath. So, because the logic of Automath has less "datatypes" built-in, in Automath the use of axioms at the start of a proof development is unavoidable.

  This in its turn causes that in Automath generally people are less inclined to stay within the constructive logic built into the system. The big proof developments that were created in the Automath project from the seventies all used classical logic.

• The type theory on which Automath is based is subtly different from the "modern" type theories that are based on the "calculus of constructions" (with its fine structure as given by the Barendregt cube.) To be specific: suppose that in some context

  x : D

  we have an expression f(x) that has type R(x) that in its turn has some type T(x), so that we have

  f(x) : R(x) : T(x)

  (actually, the variable x won't occur in the "kind" T(x), so we could just write "T".) Then in the modern systems we have

  [x:D]f(x) : (x:D)R(x) : T(x)

  (in which the "[x]" should be read as "lambda x" and the "(x)" as "Pi x".) However, in the Automath system we'd have

  [x:D]f(x) : [x:D]R(x) : [x:D]T(x)

  In some way the Automath "[]" abstractor generalizes both the lambda and Pi abstractors. Or conversely, the lambda an Pi could be seen as the first two stages of the Automath "[]". (Actually, in the Aut-QE language there is something called "type inclusion" which means that there the typing

  [x:D]R(x) : T(x)

  is also allowed, muddling this distinction between the "old" and the "new" ways of typing a lambda abstraction.)

(last modification 1999-09-29)