Proof Assistants (Automath to Coq)
Programs that check every step of a mathematical proof, from Automath (1967) to Isabelle and Coq (1980s), made it possible to trust very long proofs without a human checking each line.
Open in the interactive tree →Nicolaas de Bruijn began Automath in 1967 as a language in which whole mathematics books could be written and checked by computer, and in the 1970s L. S. van Benthem Jutting translated Landau's textbook Foundations of Analysis into it as a doctoral thesis. Andrzej Trybulec started the Mizar system around 1973, Coq was begun at INRIA in France in 1984, and Lawrence Paulson released Isabelle in 1986. A small checking program accepts a proof only if every step is correct, which allowed the Flyspeck team to verify the Kepler conjecture (2014); Lean, now popular for formal mathematics, was strongly influenced by Coq.
Prerequisites
- Set Theory & Formal Logic1874Frege's formal logic is the language in which these systems state proofs.
- Computability (Turing)1936Automath and Coq are built on Church's typed lambda calculus.
- Programming Languages1957Systems such as LCF and Coq are built as programming languages for proofs.
Unlocks
- Kepler Conjecture & Flyspeck1998-2014Flyspeck verified the proof with the proof assistants HOL Light and Isabelle.
- Formal Proofs (Lean, Rocq)2005-2026Lean is a proof assistant in the line begun by Automath, Mizar and Coq.