1. Introduction

1.1. Getting Started

The goal of this book is to teach you to formalize mathematics using the Lean 3 interactive proof assistant. It assumes that you know some mathematics, but it does not require much. Although we will cover examples ranging from number theory to measure theory and analysis, we will focus on elementary aspects of those fields, in the hopes that if they are not familiar to you, you can pick thhem up as you go. We also don’t presuppose any background in formalization. Formalization can be seen as a kind of computer programming: we will write mathematical definitions, theorems, and proofs in a regimented language, like a programming language, that Lean can understand. In return, Lean provides feedback and information, interprets expressions and guarantees that they are well-formed, and ultimately certifies the correctness of our proofs.

You can learn more about Lean from the Lean project page and the Lean community web pages. This tutorial is based on Lean’s large and ever-growing library, mathlib. We also strongly recommend taking a look at the Lean Zulip online chat group if you haven’t already. You’ll find a lively and welcoming community of Lean enthusiasts there, happy to answer questions and offer moral support.

Although you can read a pdf or html version of this book online, it designed to be read interactively, running Lean from inside the VS Code editor. To get started:

Install Lean, VS Code, and mathlib following the instructions on the community web site.
In a terminal, type leanproject get mathematics_in_lean to set up a working directory for this tutorial.
Type code mathematics_in_lean to open that directory in VS Code.

Opening any Lean file will simultaneously open this book in a VS Code window. You can update to a newer version by tying git pull followed by leanproject get-mathlib-cache inside the mathematics_in_lean folder.

Alternatively, you can run Lean and VS Code in the cloud, using Gitpod <https://gitpod.io/>. You can find instructions as to how to do that on the Mathematics in Lean project page on Github.

Each section in this book has an associated Lean file with examples and exercises. You can find them in the folder src, organized by chapter. We recommend making a copy of that folder so that you can experiment with the files as you go, while leaving the originals intact. The text will often include examples, like this one:

#eval "Hello, World!"

You should be able to find the corresponding example in the associated Lean file. If you click on the line, VS Code will show you Lean’s feedback in the Lean Goal window, and if you hover your cursor over the #eval command VS Code will show you Lean’s response to this command in a pop-up window. You are encouraged to edit the file and try examples of your own.

This book moreover provides lots of challenging exercises for you to try. Don’t rush past these! Lean is about doing mathematics interactively, not just reading about it. Working through the exercises is central to the experience. You can always compare your solutions to the ones in the solutions folder associated with each section.

1.2. Overview

Put simply, Lean is a tool for building complex expressions in a formal language known as dependent type theory.

Every expression has a type, and you can use the #check command to print it. Some expressions have types like ℕ or ℕ → ℕ. These are mathematical objects.

#check 2 + 2

def f (x : ℕ) := x + 3

#check f

Some expressions have type Prop. These are mathematical statements.

#check 2 + 2 = 4

def fermat_last_theorem :=
  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x^n + y^n ≠ z^n

#check fermat_last_theorem

Some expressions have a type, P, where P itself has type Prop. Such an expression is a proof of the proposition P.

theorem easy : 2 + 2 = 4 := rfl

#check easy

theorem hard : fermat_last_theorem := sorry

#check hard

If you manage to construct an expression of type fermat_last_theorem and Lean accepts it as a term of that type, you have done something very impressive. (Using sorry is cheating, and Lean knows it.) So now you know the game. All that is left to learn are the rules.

This book is complementary to a companion tutorial, Theorem Proving in Lean, which provides a more thorough introduction to the underlying logical framework and core syntax of Lean. Theorem Proving in Lean is for people who prefer to read a user manual cover to cover before using a new dishwasher. If you are the kind of person who prefers to hit the start button and figure out how to activate the potscrubber feature later, it makes more sense to start here and refer back to Theorem Proving in Lean as necessary.

Another thing that distinguishes Mathematics in Lean from Theorem Proving in Lean is that here we place a much greater emphasis on the use of tactics. Given that we are trying to build complex expressions, Lean offers two ways of going about it: we can write down the expressions themselves (that is, suitable text descriptions thereof), or we can provide Lean with instructions as to how to construct them. For example, the following expression represents a proof of the fact that if n is even then so is m * n:

example : ∀ m n : nat, even n → even (m * n) :=
assume m n ⟨k, (hk : n = 2 * k)⟩,
have hmn : m * n = 2 * (m * k),
  by rw [hk, mul_left_comm],
show ∃ l, m * n = 2 * l,
  from ⟨_, hmn⟩

The proof term can be compressed to a single line:

example : ∀ m n : nat, even n → even (m * n) :=
λ m n ⟨k, hk⟩, ⟨m * k, by rw [hk, mul_left_comm]⟩

The following is, instead, a tactic-style proof of the same theorem:

example : ∀ m n : nat, even n → even (m * n) :=
begin
  -- say m and n are natural numbers, and assume n=2*k
  rintros m n ⟨k, hk⟩,
  -- We need to prove m*n is twice a natural. Let's show it's twice m*k.
  use m * k,
  -- substitute in for n
  rw hk,
  -- and now it's obvious
  ring
end

As you enter each line of such a proof in VS Code, Lean displays the proof state in a separate window, telling you what facts you have already established and what tasks remain to prove your theorem. You can replay the proof by stepping through the lines, since Lean will continue to show you the state of the proof at the point where the cursor is. In this example, you will then see that the first line of the proof introduces m and n (we could have renamed them at that point, if we wanted to), and also decomposes the hypothesis even n to a k and the assumption that n = 2 * k. The second line, use m * k, declares that we are going to show that m * n is even by showing m * n = 2 * (m * k). The next line uses the rewrite tactic to replace n by 2 * k in the goal, and the ring tactic solves the resulting goal m * (2 * k) = 2 * (m * k).

The ability to build a proof in small steps with incremental feedback is extremely powerful. For that reason, tactic proofs are often easier and quicker to write than proof terms. There isn’t a sharp distinction between the two: tactic proofs can be inserted in proof terms, as we did with the phrase by rw [hk, mul_left_comm] in the example above. We will also see that, conversely, it is often useful to insert a short proof term in the middle of a tactic proof. That said, in this book, our emphasis will be on the use of tactics.

In our example, the tactic proof can also be reduced to a one-liner:

example : ∀ m n : nat, even n → even (m * n) :=
by { rintros m n ⟨k, hk⟩, use m * k, rw hk, ring }

Here we have used tactics to carry out small proof steps. But they can also provide substantial automation, and justify longer calculations and bigger inferential steps. For example, we can invoke Lean’s simplifier with specific rules for simplifying statements about parity to prove our theorem automatically.

example : ∀ m n : nat, even n → even (m * n) :=
by intros; simp * with parity_simps

Another big difference between the two introductions is that Theorem Proving in Lean depends only on core Lean and its built-in tactics, whereas Mathematics in Lean is built on top of Lean’s powerful and ever-growing library, mathlib. As a result, we can show you how to use some of the mathematical objects and theorems in the library, and some of the very useful tactics. This book is not meant to be used as an overview of the library; the community <https://leanprover-community.github.io/>_ web pages contain extensive documentation. Rather, our goal is to introduce you to the style of thinking that underlies that formalization, so that you are comfortable browsing the library and finding things on your own.

Interactive theorem proving can be frustrating, and the learning curve is steep. But the Lean community is very welcoming to newcomers, and people are available on the Lean Zulip chat group round the clock to answer questions. We hope to see you there, and have no doubt that soon enough you, too, will be able to answer such questions and contribute to the development of mathlib.

So here is your mission, should you choose to accept it: dive in, try the exercises, come to Zulip with questions, and have fun. But be forewarned: interactive theorem proving will challenge you to think about mathematics and mathematical reasoning in fundamentally new ways. Your life may never be the same.

Acknowledgments. We are grateful to Gabriel Ebner for setting up the infrastructure for running this tutorial in VS Code. We are also grateful for help from Bryan Gin-ge Chen, Johan Commelin, Julian Külshammer, and Guilherme Silva. Our work has been partially supported by the Hoskinson Center for Formal Mathematics.