Get started with Lean #

Please following the instructions in the official Lean manual to install Lean.

After this installation procedure, it is crucial to read how to start or get a Lean project. And of course you'll probably want to learn Lean!

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.

If you have issues installing Lean using the official instructions, you can also follow the following legacy instructions: