Seminar 1 – Introduction

Summary

During the first seminar, we discussed how to set up lean, and worked on the first excercises from the book Mathematics in Lean.

Setting up Lean

For setting up lean, you can install the Lean 4 extension in VS Code. To use the book Mathematics in Lean, open your terminal, cd to your prefered directory and clone the git repository.

cd your_directory_of_choice
git clone https://github.com/leanprover-community/mathematics_in_lean.git

Note that to run the last command, you need to have Git installed. You can also clone the repository from VS Code, without using the terminal.

The project uses Mathlib, which is about 8GB and contains proofs of many subjects in mathematics. Instead of compiling Mathlib locally, which can take 4 hours, you can also cache a compiled version with lake. Lake is the build tool for Lean, and should be installed automatically when installing Lean.

cd mathematics_in_lean
lake exe cache get

Now you should be ready to work on the exercises from the book. To make a copy of the exercise folder, simply copy and paste it in the same root directory.

Working with Lean

The first exercises from MIL consist of proving identities for real numbers. Note how theorems consist of a theorem name, some objects, a colon and then the statement of the theorem. To prove them, the “by” keyword switches to tactic mode. In tactic mode, we see our goal and our asssumptions that we can use to prove the goal in the Lean InfoView. For example, we have

theorem add_zero (a : R) : a + 0 = a := by

Our goal is now to show that a + 0 = a, and we have the extra information that a is of type R, which is a ring. We can then use the rewrite tactic, abbreviated as rw, together with theorems for rings from Mathlib to prove our goal. In the example, we would first use the theorem add_comm, which states that $\forall a b : R, a + b = b + a$.

  rw [add_comm]

This replaces the left hand side of add_comm, where $a = a$ and $b = 0$, by the right hand side of the equality. Hence, our goal changed from $a + 0 = a$ to $0 + a = a$. Next, we use the theorem zero_add, showing that $\forall a : 0 + a = a$.

  rw [zero_add]

Now, our goal changed to $a = a$, which is accepted as the end of the proof. To use theorems like add_comm for replacing the RHS by the LHS, you can type

  rw [← add_comm]

Here, the symbol $\leftarrow$ can by typed as \l. The exercises introduce many other tactics and theorems, and we plan to set up a github with a summary of these in one of the next Lean seminars.

For next week

As a homework for the next time, try to finish this section and see how far you can get with “2.2. Proving Identities in Algebraic Structures”. At the beginning of the next session, we will start by discussing how it went so far and what obstacles did you encounter.