Post 3: Lean

24 Dec 2023

In this post I’m going to talk about the proof assistant Lean, what I’ve done with it, and what I hope to do with it.

First, here are some relevant links; they all open in a new tab. This is the link to the page where you can download Lean and view its documentation. This is the community page, with a bunch of information about what Lean is and how to start learning it. There is also a Zulip chatroom dedicated to Lean; it is very active and friendly.

My first introduction to Lean was with the natural number game, which you can find here (opens in new tab). This “game” teaches you the basics of Lean by starting with the axioms of natural numbers and proving basic facts, such as addition and multiplication are commutative. It also teaches you how functions and propositions work in Lean. I really recommend it as a starting point. It is completely web based; you don’t need to download Lean. The link also contains a set theory game.

When working in Lean, you essentially have two toolboxes. The first toolbox is the collection of tactics. These range from basic functionality that you need to do anything, to powerful functions that can take care of tedious algebraic or logical manipulations. The second toolbox is the collection of theorems¹ that have been proven. In practice², this collection is known as mathlib. Essentially, the goal of mathematicians working with Lean is to expand mathlib as much as possible.

The workflow in Lean is as follows. You have some result you want to prove; it has hypotheses and a conclusion. Here is the first example from the Lean 3 version of the natural number game, adapted to Lean 4:

lemma example1 (x y z : mynat) : x * y + z = x * y + z := by

The result is named example1. The hypotheses are that you have x, y, and z which are elements³ of mynat, which is the game’s version of the natural numbers. The conclusion is that x*y+z=x*y+z. The keyword by tells Lean that the proof will come directly after.

So, how do you prove this result? Well, notice that the conclusion is of the form a=a. By definition of equality, this statement must be true. The way to assert that is with the tactic rfl. For instance, this is a complete proof of example1:

lemma example1 (x y z : mynat) : x * y + z = x * y + z := by
    rfl

Another part of the Lean workflow is the “infoview”, as it is called in VSCode. As you progress through a proof, it will show you your available hypotheses and goal(s). A proof is finished when there are no goals.

I won’t get into anything more specific than that example. As I said before, I suggest playing the natural number game to get a feel for Lean.

Finally, I want to discuss what I hope to do in Lean. First, I need to learn more. I will work through the set theory game, as I didn’t know it existed until I wrote this post. I will also work through the interactive book, creatively called Mathematics in Lean (opens in new tab). Then, I want to formalize⁴ some of the basic representation theory topics that haven’t been formalized yet, c.f. this list (opens in new tab). After that, if I don’t wear myself out, I might try my hand at harder topics, like algebraic geometry and geometric representation theory.

I’ll write more if and when I start contributing to the Lean community, but for now, that’s all I have to say.

Footnotes: