Lean is a new open source theorem prover being developed at Microsoft Research, and its standard library at Carnegie Mellon University. Lean 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. The goal is to support both mathematical reasoning and reasoning about complex systems, and to verify claims in both domains.

The Lean project was launched by Leonardo de Moura at Microsoft Research in 2013. It is a collaborative open source project, hosted on GitHub. Contributions to the code base and library are welcome.

You can experiment with an online version of Lean that runs in your browser, or try the online tutorials listed under documentation.