Set up 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 can try running it in the cloud using Gitpod or GitHub Codespaces. For instance, you can read the book Mathematics in Lean while doing the exercises on Gitpod. Note this Gitpod option requires you to create an account somewhere. Note also that Gitpod is being deprecated in April 2025.
Installing Lean and creating a project #
The important thing to know about a local installation is that it is a two-step process. First you need to install the software. But this is not enough; to run Lean on a file, the file must be part of a Lean project.
Once you have installed Lean, you can either install a Lean project from the internet (for example the Mathematics in Lean project) or you can create your own project.
The recommended way to install Lean and to get working with a project is to follow the instructions in the official Lean manual. The manual explains a simple point-and-click method for both installing Lean, and creating or downloading a project.
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.