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 45 articles , 2 standard articles )

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

1 2 3 next

  1. Bauer, Andrej; Petković Komel, Anja: An extensible equality checking algorithm for dependent type theories (2022)
  2. Wieser, Eric; Song, Utensil: Formalizing geometric algebra in Lean (2022)
  3. Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
  4. Carranza, Daniel; Chang, Jonathan; Kapulkin, Chris; Sandford, Ryan: 2-adjoint equivalences in homotopy type theory (2021)
  5. de Moura, Leonardo; Ullrich, Sebastian: The Lean 4 theorem prover and programming language (2021)
  6. Fervari, Raul; Trucco, Francisco; Ziliani, Beta: Verification of dynamic bisimulation theorems in Coq (2021)
  7. Kohlhase, Michael; Rabe, Florian: Experiences from exporting major proof assistant libraries (2021)
  8. Mahboubi, Assia; Sibut-Pinote, Thomas: A formal proof of the irrationality of (\zeta(3)) (2021)
  9. Rabe, Florian: A language with type-dependent equality (2021)
  10. Reed Oei, Dun Ma, Christian Schulz, Philipp Hieronymi: Pecan: An Automated Theorem Prover for Automatic Sequences using Büchi Automata (2021) arXiv
  11. Xu, Runqing; Li, Liming; Zhan, Bohua: Verified interactive computation of definite integrals (2021)
  12. Abel, Andreas; Coquand, Thierry: Failure of normalization in impredicative type theory with proof-irrelevant propositional equality (2020)
  13. Avigad, Jeremy: Modularity in mathematics (2020)
  14. Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert: Designing normative theories for ethical and legal reasoning: \textscLogiKEyframework, methodology, and tool support (2020)
  15. Cockx, Jesper; Abel, Andreas: Elaborating dependent (co)pattern matching: no pattern left behind (2020)
  16. De Lon, Adrian; Koepke, Peter; Lorenzen, Anton: Interpreting mathematical texts in Naproche-SAD (2020)
  17. Kahl, Wolfram: Calculational relation-algebraic proofs in the teaching tool \textscCalcCheck (2020)
  18. Meshveliani, S. D.: On a machine-checked proof for fraction arithmetic over a GCD domain (2020)
  19. van den Berg, Benno: Univalent polymorphism (2020)
  20. van Doorn, Floris; Ebner, Gabriel; Lewis, Robert Y.: Maintaining a library of formal mathematics (2020)

1 2 3 next