Lean is an interactive formal theorem proving language (abbreviated as ITP), initiated by Leonardo de Moura in 2014. ITPs allow users to state and prove mathematical statements in a language that is then “compiled” (type-checked), to verify its correctness. Mathlib is a comprehensive library developed as a project supplementary to the Lean language itself, providing a wide range of mathematical theories and tools that facilitate theorem proving and exploration within the Lean environment. This post is only intended as the most basic of introductions to get you set up and started to follow along this project. For other more complete resources, check out the official community page.

The most common approach to working with Lean 4 uses Visual Studio Code with the Lean 4 extension installed. The extension gives you syntax highlighting and the Lean infoview, but it also automatically sets up Lean 4 on your system and makes some commands available in your terminal: lean serves as the core command-line interface for interacting with Lean files, lake is Lean’s build and package manager essential for creating, managing, and compiling Lean projects, and elan is a version manager for Lean, allowing your to switch between different Lean versions or configurations for project-specific compatibility.

Creating your own project

To start a new Lean 4 project, for example MyLeanProject, run lake new MyLeanProject math. This creates a new folder, containing some initial files, in particular lakefile.lean, which sets project settings and dependencies, lean-toolchain, which specifies the Lean version used in this project, MyLeanProject.lean, which serves as the root module of the MyLeanProject library and is used to import and organize modules within the project, and MyLeanProject/Basic.lean, an example Lean file in a subdirectory that illustrates project organization and can be used to start adding your Lean code.

1
2
3
4
5
6
MyLeanProject
├── lakefile.lean
├── lean-toolchain
├── MyLeanProject
│   └── Basic.lean
└── MyLeanProject.lean

If you check lakefile.lean, you will see the line require mathlib from git "https://github.com/leanprover-community/mathlib4.git", which means that your project already has mathlib and all of its formal math as a dependency (this is what the optional math argument was for when creating the new project). Running lake build you will see that first the dependencies are copied into the hidden folder .lake/packages and then your project is built.

How to prove a statement

Let us go through how one would add code to this project to prove the most basic of examples, namely that the sum of two even numbers is even. Open the file MyLeanProject/Basic.lean and remove its current content. The Lean infoview should pop up and note that there is No info found. We start by importing mathlib’s notion of parity through import Mathlib.Data.Int.Parity. This allows us to state the desired theorem through

1
2
3
4
5
theorem sum_of_even_is_even 
  (a b : ℤ) 
  (ha : Even a) 
  (hb : Even b) 
: Even (a + b) := by sorry

Taken literally, the statement reads that for any given \(a, b \in \mathbb{Z}\) s.t. \(a\) is even and \(b\) is even, their sum \(a+b\) is even. The sorry acts as a placeholder for a proof that hasn’t been formulated yet. Putting your cursor at the beginning of the proof, before sorry, gives you an overview of your current assumptions and goals in the infoview on the right:

1
2
3
4
5
1 goal
ab: ℤ
ha: Even a
hb: Even b
⊢ Even (a + b)

Remove the sorry and go to the next line. As you add arguments to your proof, the assumptions and goals will change. One possible, if slightly verbose, proof could look something like this:

1
2
3
4
5
6
rw [Even] at *
let ⟨s, hs⟩ := ha
let ⟨t, ht⟩ := hb
use s + t
rw [hs, ht]
simp only [←add_assoc, ←two_mul, ←mul_add]

This proof first of all applies the definition of evenness to rewrite (rw) the assumptions and goals. Turns out a natural number \(n\) is even in mathlib if \(n = r + r\) for some \(r \in \mathbb{N}\). We let the respective \(r\)s corresponding to \(a\) and \(b\) be denoted by \(s\) and \(t\) and then use their sum \(s+t\) as the \(r\) required for \(a+b\). What remains is to rewrite (rw) the goal using \(a = s + s\) and \(b = t + t\) followed by some basic, if slightly annoying, application of properties of the addition of natural numbers.

Of course, this seems awfully complicated and there are many ways in which one could have simplified this by invoking existing statements in mathlib and through tools built into mathlib that can make suggestions. Running exact? at the beginning of the proof for example suggests the one line proof exact Int.even_add.mpr { mp := fun a ↦ hb, mpr := fun a ↦ ha }. Here one can already tell that proofs in Lean can appear significantly more obfuscated than our small example might indicate. We will generally strive for more readable and idiomatic proofs with the goal of staying close to the chain of logic as presented in the non-formal form of the proof. In particular, this implies that our proofs will not be the shortest, most compact possible versions possible nor will they necessarily adhere to common practices for contributing to mathlib.

Working on an existing project

To follow along with or contribute to an existing project, you would usually start by cloning the corresponding git repository to your local machine. For instance, if you’re interested in closely following the examples from this blog, you should start by running git clone https://github.com/FordUniver/thebook.lean. This will create a local copy of the project on your machine. After cloning, navigate into the project directory with and run lake update to fetch the latest versions of all dependencies. If you check the lakefile.lean of any particular project, you will commonly find that the mathlib dependency is fixed to a specific version, so that changes in mathlib don’t immediately break the work on your project.