Automath

This article is about the programming language. For self-taught individuals, see Autodidacticism.

Automath (automating mathematics) was a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness. The Automath system included many novel notions that were later adopted and/or reinvented in areas such as typed lambda calculus and explicit substitution. Dependent types is one outstanding example. Automath was also the first practical system that exploited the Curry–Howard correspondence. Propositions were represented as sets (called "categories") of their proofs, and the question of provability became a question of non-emptiness (type inhabitation); de Bruijn was unaware of Howard's work, and stated the correspondence independently.

L.S. Jutting, as part of this Ph.D. thesis in 1976, translated Edmund Landau's Foundations of Analysis into Automath and checked its correctness.

Automath was never widely publicized at the time, however, and so never achieved widespread use; nonetheless, it proved very influential in the later development of logical frameworks and proof assistants. The Mizar system, a system of writing and checking formalized mathematics that is still in active use, was influenced by Automath.

History

In 1967, De Bruijn had designed a first version of a formal language for mathematics: the Primitive Automatic Language(PAL). It already contained most of the basic ideas for such a language. A book in PAL was formed by lines of text organized in nested blocks. Lines could be either axioms, type declarations for variables, or definitions. Surprisingly, with this simple structure one can represent real pieces of mathematics: basically everything that does not exploit the modern notion of function. In fact, in retrospect PAL can be seen as the definition system present in the Automath languages. By extending PAL in 1968 with the λ-notation for functions, which De Bruijn became acquainted with through the analysis courses of his colleague H. Freudenthal of Utrecht University, he incorporated the modern notion of function aswell. This resulted in basic Automath which was later renamed as AUT-68.

The research stimulated by the design of the Automath language and some of its variants became bundled in the so called Automath project, in which a number of researchers joined forces. The Automath project was initiated and was led by De Bruijn in Eindhoven from 1967 until the early 1980s. Readers who were interested in a more complete historical and scientific account of the project are referred to the collection Selected Papers on Automath and to the Automath Archive. Both include several retrospective articles by De Bruijn and others involved in the project. Some recent workshops containing historical reviews are Thirty Five Years of Automating Mathematics and Mathematics, Logic and Computation

De Bruijn’s central aim with the project was the design of a formal language in which any piece of mathematics can be straight forwardly expressed, with the property that a computer can check the correctness of the text. The use of the system should be close to mathematical practice and should not depend on any foundational paradigm for mathematics. The project aimed beyond showing that such a thing was theoretically possible. De Bruijn was convinced it was actually feasible, even with the computers of the time and he was anxious to show this. His dream was that within one or two decades that mathematicians would have a proof checker on their desk and that they would actually use for verifying and archiving results. And which possibly also would assist the mathematician in proving new results. These goals were quite different from other projects in the emerging field of reasoning with computers, as De Bruijn himself noticed at the conference on Automatic Deduction at Versailles, France in 1968. The vast majority of these projects were more ambitious, automated theorem proving such as automatic generation of proofs rather than the humbler task of verification of proofs that already have been delivered. The formal languages in the proof-generating ventures were necessarily of restricted and specialized expressive power so as to keep the system decidable. Therefore they would never be able to capture entire areas of mathematics, as De Bruijn desired. But the Automath project has made lasting contributions, such as:

• Independence of logic: it suffices (and is also advantageous) to design a logical framework suited to different kinds of logical systems.

• Venturing ‘‘beyond Gödel’’: computers can be useful for mathematics, even if they cannot solve all mathematical problems by themselves.

• Enhanced reliability: the feature that all obtained formal expressions can be checked by one fixed and relatively easy algorithm, which can be validated beforehand once and for all.

The Automath project demonstrated that automatic verification of mathematics was feasible, even with the computer technology of the early 1970s. However, the achievements of the project were not appreciated at the time. Only two decades later, De Bruijn’s work was picked up by a new generation of researchers. They recognized the valuable insights underlying the Automath project, and they applied them in their own work.De Bruijn’s pioneering ventures with Automath are nowadays widely appreciated, in particular in the community of applied logicians working in type theory and in verification of mathematical theories and computer programs.

See also

• QED manifesto

External links

• The Automath Archive (mirror)
• Thirty Five years of Automath homepage of a workshop to celebrate the 35th year of Automath
• Automath page by Freek Wiedijk