Lean

The Lean theorem prover (system description). Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a rich API which can be used to embed it into other systems. It is currently being used to formalize category theory, homotopy type theory, and abstract algebra. We describe the project goals, system architecture, and main features, and we discuss applications and continuing work.


References in zbMATH (referenced in 26 articles , 2 standard articles )

Showing results 1 to 20 of 26.
Sorted by year (citations)

1 2 next

  1. Avigad, Jeremy: Modularity in mathematics (2020)
  2. Cockx, Jesper; Abel, Andreas: Elaborating dependent (co)pattern matching: no pattern left behind (2020)
  3. van den Berg, Benno: Univalent polymorphism (2020)
  4. Ebner, Gabriel: Herbrand constructivization for automated intuitionistic theorem proving (2019)
  5. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  6. Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico: Implementing type theory in higher order constraint logic programming (2019)
  7. Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
  8. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  9. Rahli, Vincent; Bickford, Mark; Cohen, Liron; Constable, Robert L.: Bar induction is compatible with constructive type theory (2019)
  10. Angiuli, Carlo; Harper, Robert: Meaning explanations at higher dimension (2018)
  11. Buchholtz, Ulrik; Rijke, Egbert: The Cayley-Dickson construction in homotopy type theory (2018)
  12. Carette, Jacques; Farmer, William M.; Sharoda, Yasmine: Biform theories: project description (2018)
  13. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  14. Lochbihler, Andreas; Schneider, Joshua: Relational parametricity and quotient preservation for modular (co)datatypes (2018)
  15. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  16. Carter, Nathan C.; Monks, Kenneth G.: A web-based toolkit for mathematical word processing applications with semantics (2017)
  17. Ford, Ian: Semantic representation of general topology in the Wolfram language (2017)
  18. Fulton, Nathan; Mitsch, Stefan; Bohrer, Brandon; Platzer, André: Bellerophon: tactical theorem proving for hybrid systems (2017)
  19. Nagashima, Yutaka; Kumar, Ramana: A proof strategy language and proof script generation for Isabelle/HOL (2017)
  20. van Doorn, Floris; von Raumer, Jakob; Buchholtz, Ulrik: Homotopy type theory in Lean (2017)

1 2 next