Options to use Lean #
There are two ways for you to start interacting with Lean. Installing it on your own computer will give you the most satisfactory experience. However, some Lean projects offer ways of interacting with them via the cloud, which requires no local installation.
Without a local installation #
If you only want to try Lean without installing it, you have a couple of options. If you want to do a quick one-off experiment, you can use the Online Lean editor. If you want to work on a bigger project you can use GitHub Codespaces (or Gitpod, but that is deprecated as of April 2025). For instance, you can read the book Mathematics in Lean while doing the exercises on GitHub Codespaces. Note this requires you to create an account on GitHub.
Installing Lean #
Click here for the instructions to install Lean.
After you have followed these instructions, you'll probably want to learn Lean!
Command line #
The community used to maintain its own installation instructions. These contain more low-level instructions on how to install Lean and to create projects. They may be out of date.