You can experiment with Lean by running an online Javascript version in your browser. If you have installed Lean locally, you can use it interactively with Visual Studio Code or Emacs. See the Using Lean chapter of the reference manual for details.

Lean is a work in progress. You are welcome to experiment with it, but please recognize that the system is still changing, and if you are looking for stability, it may not be the system for you. Similarly, the project cannot accommodate feature requests at this stage. If you are trying to decide whether to invest time in learning to use Lean right now, this FAQ may be helpful.


Each of the following tutorials is available in an online version that runs alongside a Lean in your browser, and as a PDF document. The most comprehensive is the following:

  • Theorem Proving in Lean
    A introduction to using Lean as an interactive theorem prover.
    online tutorial, pdf

The next two are incomplete and outdated but may be helpful:

  • An Introduction to Lean
    A quick tour of Lean and its features.
    online tutorial, pdf

  • Programming in Lean
    An introduction to writing and reasoning about programs in Lean, as well as writing tactics and automation.
    online tutorial, pdf

Reference (work in progress)

The current version of Lean is Lean 3, its development is frozen. The source code and libraries can be found on github. The next version of Lean will be released when it is ready.

Lean 2

The previous version of Lean, Lean 2, is still being maintained but not developed. Lean 2 has special support for homotopy type theory and a substantial library. The source code and libraries can be found on github.

Chat Room

A public chat room dedicated to Lean is open on Zulip.


You are welcome to join the Lean user forum on Google Groups.