Creating a Lean project #

Lean files are organized in projects called packages. Projects are git repositories containing a leanpkg.toml file specifying the Lean version and all required dependencies alongside the src/ subdirectory containing the Lean code. The tool leanproject manages project creation and dependencies.

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.

Working on an existing package #

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

Contributing to mathlib #

See How to contribute to mathlib.