Automath ("automating mathematics") is a
formal language
In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules.
The alphabet of a formal language consists of sy ...
, devised by
Nicolaas Govert de Bruijn
Nicolaas Govert (Dick) de Bruijn (; 9 July 1918 – 17 February 2012) was a Dutch mathematician, noted for his many contributions in the fields of analysis, number theory, combinatorics and logic. starting in 1967, for expressing complete mathematical theories in such a way that an included automated
proof checker
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
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
A typed lambda calculus is a typed formalism that uses the lambda-symbol (\lambda) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a ...
and
explicit substitution In computer science, lambda calculus, lambda calculi are said to have explicit substitutions if they pay special attention to the formalization of the process of substitution of variables, substitution. This is in contrast to the standard lambda cal ...
.
Dependent types
In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers lik ...
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 rela ...
. 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 \Gam ...
); 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
Edmund Georg Hermann Landau (14 February 1877 – 19 February 1938) was a German mathematician who worked in the fields of number theory and complex analysis.
Biography
Edmund Landau was born to a Jewish family in Berlin. His father was Leopol ...
'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 assistant
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
s.
[F. Kamareddine (2003) ''Thirty-five years of automating mathematics.'' Workshop, Dordrecht, Boston, published by Kluwer Academic Publishers, .] The
Mizar system
The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in ...
, a system of writing and checking formalized mathematics that is still in active use, was influenced by Automath.
See also
*
QED manifesto
The QED manifesto was a proposal for a computer-based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically. ( Q.E.D. means in Latin, meaning "which was to be demonstrated.")
Overview
T ...
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