constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
= + +
| / | -/ | |
| , | ||
| of / of | ||
| for | for hom-tensor adjunction | |
| introduction rule for | for hom-tensor adjunction | |
| ( of) | ( of) | |
| into | into | |
| ( of) | ( of) | |
| , , | ||
| higher | ||
| / | -// | |
| / | ||
| , () | , | |
| (, ) | / | |
| (absence of) | (absence of) | |
Lean is a proof assistant based on dependent type theory. Like Coq and Agda, it may be used to implement homotopy type theory.
Lean libraries for HoTT include:
and implementation in Lean is in
Lean website (leanprover.github.io)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer, The Lean Theorem Prover (system description) (pdf)
Jeremy Avigad, Leonardo de Moura, Soonho Kong, Theorem Proving in Lean (pdf)
Robert Y. Lewis, Leonardo de Moura, Automation and Computation in the Lean Theorem Prover, contribution to HaTT 2016: Hammers for Type Theories, 2016 (pdf)
Thomas Hales, A Review of the Lean Theorem Prover, September 2018
Kevin Buzzard, Xena project (2018)
Last revised on January 8, 2019 at 11:43:29. See the history of this page for a list of all contributions to it.