You can experiment with Lean by running an online Javascript version in your browser (see also the community version). 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.

The learning resources page of the community website lists many tutorials and documentation sources.

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.