×

Lean

swMATH ID: 15148
Software Authors: Microsoft; de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob
Description: 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.
Homepage: https://leanprover.github.io/about/
Source Code: https://github.com/leanprover/lean
Related Software: Coq; Isabelle/HOL; Agda; HOL Light; Mizar; PVS; Isabelle; HOL; MMT; GitHub; Idris; Archive Formal Proofs; z3; Mathematica; kepler98; Matita; cubicaltt; mathlib; QMT; Nitpick
Cited in: 53 Publications
all top 5

Cited by 107 Authors

5 de Moura, Leonardo
4 van Doorn, Floris
3 Buchholtz, Ulrik
3 Kaliszyk, Cezary
3 Rabe, Florian
3 von Raumer, Jakob
2 Abel, Andreas M.
2 Avigad, Jeremy
2 Carette, Jacques
2 Cockx, Jesper
2 Ebner, Gabriel
2 Farmer, William M.
2 Kohlhase, Michael
2 Lewis, Robert Y.
2 Lochbihler, Andreas
2 Meshveliani, S. D.
2 Paulson, Lawrence Charles
2 Rijke, Egbert
2 Ullrich, Sebastian
1 Angiuli, Carlo
1 Barrett, Clark W.
1 Bauer, Andrej
1 Benzmüller, Christoph Ewald
1 Bickford, Mark
1 Blanchette, Jasmin Christian
1 Bohrer, Brandon
1 Boldo, Sylvie
1 Bordg, Anthony
1 Bouzy, Aymeric
1 Bright, Curtis
1 Browning, Thomas L.
1 Buzzard, Kevin
1 Carranza, Daniel
1 Carter, Nathan C.
1 Chang, Jonathan
1 Clément, François
1 Cohen, Liron
1 Constable, Robert Lee
1 Coquand, Thierry
1 Czajka, Łukasz
1 Czarnecki, Krzysztof
1 De Lon, Adrian
1 Devriese, Dominique
1 Faissole, Florian
1 Fervari, Raul
1 Fontaine, Pascal
1 Ford, Ian J.
1 Fulton, Nathan
1 Ganesh, Vijay
1 Gauthier, Thibault
1 Grayson, Daniel Richard
1 Guidi, Ferruccio
1 Harper, Robert
1 Heinle, Albert
1 Hirata, Michikazu
1 Holliday, Wesley H.
1 Hughes, Chris
1 Kahl, Wolfram
1 Kapulkin, Chris
1 Koepke, Peter
1 Kong, Soonho
1 Kotsireas, Ilias S.
1 Kumar, Ramana
1 Lau, Kenny
1 Li, Liming
1 Li, Wenda
1 Livingston, Amelia
1 Lorenzen, Anton
1 Lutz, Patrick
1 Mahboubi, Assia
1 Martin, Vincent
1 Mayero, Micaela
1 Minamide, Yasuhiko
1 Mir, Ramon Fernández
1 Mitsch, Stefan
1 Monks, Kenneth G.
1 Nagashima, Yutaka
1 Nejati, Saeed
1 Nipkow, Tobias
1 Norman, Chase
1 Pacuit, Eric
1 Pąk, Karol
1 Parent, Xavier
1 Petković Komel, Anja
1 Piessens, Frank
1 Platzer, André
1 Popescu, Andrei
1 Rahli, Vincent
1 Sacerdoti Coen, Claudio
1 Sandford, Ryan
1 Sato, Tetsuya
1 Schneider, Joshua P.
1 Selsam, Daniel
1 Sharoda, Yasmine
1 Sibut-Pinote, Thomas
1 Song, Utensil
1 Tassi, Enrico
1 Traytel, Dmitry
1 Trucco, Francisco
1 Van den Berg, Benno
...and 7 more Authors

Citations by Year