This webpage is about Lean 3, which is effectively obsolete; the community has migrated to Lean 4.

Jump to the corresponding page on the main Lean 4 website.

Lean projects #

In general, if you just open a single .lean file in your text editor and try to compile it, you'll get a bunch of confusing errors. Every non-trivial piece of Lean code needs to live inside a Lean project (sometimes also called a Lean package). A "Lean project" is more than just a folder that you've named "My Lean stuff". Rather, it's a folder containing some very specific things: in particular, a git repository and a file leanpkg.toml that gathers information about dependencies of the project, including for instance the version of Lean that should be used.

If you're interested in contributing to mathlib you only need to set up a Lean project once, which you can use for all your contributions — you don't need to set up a new Lean project for each new contribution.

Setting up and managing all this is done by a little python program called leanproject. This page describes the basic use of this tool, and should be sufficient for everyday use. If this is not enough for your purposes, you can read the full leanproject documentation. If you are really curious, you can also read how pieces fit together.

There is a video walkthrough of these instructions on YouTube.

Working on an existing project #

Suppose you want to work on an existing project. As example, we will take the tutorial project. Open a terminal.

Creating a Lean project #

We will now create a new project depending on mathlib. The following commands should be typed in a terminal.

If you want to make sure everything is working, you can start by creating, say my_project/src/test.lean containing:

import topology.basic

#check topological_space

When the cursor is on the last line, the right hand part of VS Code should display a "Lean Goal" area saying: topological_space : Type u_1 → Type u_1

If, for some reason, you happen to lose the "Lean Goal" area, you can get it back with Ctrl-Shift-Enter (Cmd-Shift-Enter on MacOS). Also, you can get the Lean documentation inside VS Code using Ctrl-Shift-p (Cmd-Shift-p on MacOS) and then, inside the text field that appears, type "lean doc" and hit Enter. Then click "Theorem Proving in Lean" and enjoy.

Hosting your project on GitHub #

Your project is already a git repository, and as it grows, you may want to host it on GitHub. If you take this step, the community offers some GitHub Actions scripts that could help manage your repository. But don't worry if you don't know what this means. It's not necessary for using Lean.

Contributing to mathlib #

See How to contribute to mathlib.