Automath ("automating mathematics") is 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.
Overview
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
In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relati ...
. Propositions were represented as sets (called "categories") of their proofs, and the question of provability became a question of non-emptiness (
type inhabitation In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem: given a type \tau and a typing environment \Gamma, does there exist a \lambda-term M such that \Ga ...
); de Bruijn was unaware of Howard's work, and stated the correspondence independently.
L. S. van Benthem 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.
[F. Kamareddine (2003) ''Thirty-five years of automating mathematics.'' Workshop, Dordrecht, Boston, published by Kluwer Academic Publishers, .] The
Mizar system, a system of writing and checking formalized mathematics that is still in active use, was influenced by Automath.
See also
*
QED manifesto
References
External links
The Automath Archive(mirror)
Thirty Five years of Automathhomepage of a workshop to celebrate the 35th year of Automath
Automath pageby Freek Wiedijk
Proof assistants
Type theory
{{Formalmethods-stub