Lean Into Lean

I had been trying to get into Lean. It’s an interactive theorem prover, and I’ve been curious about it since I first heard about it during a talk by Kevin Buzzard himself.

We were fortunate to have an in-person workshop about Lean recently and I have some notes! Let the lack of organisation and detail be a reflection of how little experience and knowledge I have of Lean. Be sure to keep that in mind while reading.

1. It’s not magic.

Lean is not a tool to help prove theorems for us. It’s more of a way to get the computer to check your proof. However, if it knows the goal, there are ways to make it fill in the blanks for us. That’s more for convenience than breakthroughs. Don’t expect to use Lean to do homework or crack an unsolved problem. Do expect it to be useful to verify your solution when you do do your homework or attempt that problem!

2. Interactive?

Lean is an interactive theroem prover. The way we interact with it is by moving around and editing text on one side of the window, which manipulates the state on the other side of the window. Moving the cursor down line by line shows how each line affected the state.

3. If unsure, go with VS Code!

You can use it with VS Code, Neovim, or Emacs. I have no idea about Emacs, but the VS Code integration is far ahead of the Neovim on. The extension in VS Code provides a lot of helpful tooltips on hovering over text, makes it easy to understand complex statements, and lets you jump to definitions of tactics and types if you want to. Since these features are mostly coming from the LSP server implemented by Lean, I’m sure all that is possible with the current Nvim plugin, or even any other LSP plugin for Vim, but it takes absolutely no effort to get it working in VS Code. So far I haven’t switched to it yet, but I would recommend you begin in VS Code.

4. Syntax needs patience.

I find the syntax a little hard to get used to. Stick to it, and you’ll get a hang of it.

5. Try the Natural Number Game!

The Natural Number Game has a version for Lean 3 as well as Lean 4. I found it really helpful for practice, as well as to understand how to use it.

6. In fact all of Lean is like a game!

Once we have written our hypothesis and our goal (aka claim) lean breaks it down for us on the right hand side. Each statement we write will change something there. We might be able to conclude something which will then be populated into the list of assumptions. We can ask it to break a goal into multiple simpler ones, which will add to the list of goals. Line-by-line we can either bring the goal closer or push our assumptions farther until they meet and we’ve won!

7. aesop?, simp? and apply?

Use these tactics for hints on getting yourself out of a jam.

8. Debugging using have :=

There’s no print in Lean, nor is there a debugger. Most of the times the Infoview pane on the right is enough to tell us what we want to know. Still, there are times when it’s necessary to know what some syntax means, or just to understand the pieces that make up a complex statement. At such places/times, use the command

have := (foo x).1`

This will create a new variable called this with the value of (foo x).h. If (foo x). is not valid Lean, then of course, this won’t work.

9. The error messages make sense.

Read and parsed carefully, they mostly do tell us which direction to move in. I wish they could tell me exactly what to do, but maybe they do, and I’m not good enough with Lean to understand.

10. Don’t get intimidated by the ?m.456 ’s in the error messages.

There’s probably nothing wrong with your installation or the editor. Those are just placeholders for arguments/types (those are the same things, I think).

11. Read the docs!

Lean itself and Mathlib has documentation. It’s really helpful to be able to read it. Trust me, this helps in the long run.

12. The community is great

You can join the Lean Zulip and post questions there!

Although I think it’s a useful skill to have, Lean is fun too, and I hope you enjoy learning and using it!