Skip to main content
PRL Project

N. G. DeBruin

Automath is a language which we claim to be suitable for expressing very large parts of mathematics, in such a way that the correctness of the mathematical contents is guaranteed as long as the rules of grammar are obeyed.

Since the notions "mathematics" and "expressing" are rather vague, we had better discuss a specific example. Assume we have a very elaborate textbook on complex function theory presenting everything from scratch. That is, we start with chapters on logic and inference rules, set theory, the number systems, some geometry, some topology, some algebra, and we never use anything that is not derived, unless it has been explicitly stated as an axiom. Assume the book has been most meticulously written, without leaving a single gap. Then we claim it is possible to translate this text line by line into Automath. The grammatical correctness of this new text can be checked by a computer, and that can be considered as a final complete check of the given piece of mathematics. Moreover we claim that it is possible to do so in practice. The line by line translation will be a matter of routine; the main difficulty lies in the detailed presentation of such a large piece of mathematics. The mere labour involved in the translation will not increase if we proceed further into mathematics.

Automath was developed in 1967-1968 at the Eindhoven University of Technology, The Netherlands. The author is indebted to Mr. L. S. van Benthem Jutting for very valuable help in trying out the language in several parts of mathematics, and both to him and to Mr. L. G. F. C. van Bree for their assistance with the programming (in ALGOL) of processors by means of which books written in Automath can be checked. In particular, Mr. Jutting is currently translating Landau's "Grundlagen der Analysis".