On the Lean proof assistant, Part 1

A long time ago I became interested in proof assistants. I tried Isabelle and Coq for sure and I might have tried Mizar. Here, ‘try’ could mean tried to install and failed. Some of them worked, but I quickly gave up using them. In all of them the documentation was bad and I couldn’t figure out out to prove anything.

A while ago I heard about Lean. According to the official website,

Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.

A proof assistant is a program in which you type mathematics in a formal language and the computer checks every step using basic rules. Theoretically, such assistants may also aid in proving things, rather than just checking for correctness.

Despite my bad experience with proof assistants in the past, I decided to try Lean. I watched a talk by Kevin Buzzard, in which he claims proof assistants are the future of mathematics because math is so complicated these days that errors are bound to creep in. I’ll probably have a lot to say about that in this post and maybe others but for now let me review Lean.

Installation

There is an installation page and there is also a random binary package. I tried the installation instructions. The good news is that Lean installed, although for some reason I still cannot access the mathlib library despite following every step (more on that another time).

The installation is basically copying a bunch of code into a terminal. I had a better experience with this installation compared to some other assistants in the past, because it worked. However, it’s still pretty bad. The user should not have to install a bunch of random programs from the command line, retrieving scripts that then run and do something else. I was pretty disappointed by this and I am sure the typical mathematician who wants to get to proving stuff will just forget about it and go back to proving theorems by hand.

If the Lean community actually wants widespread adoption, or if some mathematicians want this, the installation should be painless on all platforms: either a single install package like an AppImage or installation wizard. Sage works this way: you can just unzip a package and start using it.

Visual Studio Code

There are two ways to use Lean: using Emacs or Visual Studio Code. I chose VS Code. The Lean installation installs a VS Code extension that gives you a very basic IDE environment for Lean.

The environment is basically a fancy way to display error messages and doesn’t do much else, at least on first glance. It’s kind of ugly and even TeX error messages are better. Hopefully down the road there will be a nice cross-platform GUI that allows you to structure proofs. Programmers might be fine with creating a bunch of files to structure a program, but trying to force mathematics to work like programming may not work very well, and I say this as someone who is proficient in several programming languages.

So, I think the VS Code interface is good overall, but it will need a lot of improvement for real-world mathematics use cases.

Writing proofs

I had no idea what I was doing when I started working with Lean, so I started to read the documentation and find tutorials.

Sadly, the documentation is not suitable for mathematicians trying to prove things. To put things in perspective, imagine you want to learn to paint pretty landscapes for the first time, and you’ve never picked up a brush. Now someone gives you a book on how to make paint by mixing Hawaiian volcanic island dust with the droppings of the Dodo. That’s how useful the Lean documentation is.

For example, it seems the introduction is full of code like “#check 0”, which tells you that 0 is a natural number. Then there is a War and Peace length tome telling you what types are. It’s useful information you might eventually have to know but it’s not very interesting for a mathematician.

There should be a tutorial on how to write proofs, starting with specific proofs. Actually, it is not that hard to write proofs in Lean, at least not simple ones. Now, I will preface this by saying I took quite a few courses in logic, which included natural deduction. If I did not then I probably would have given up. However, I finally wrote a proof in Lean (inserted as an image because the symbols in Lean keep showing up as question marks if I try and post the text):

Writing ‘theorem’ at the start begins a new theorem. You have to call it something so I called it ‘distribute’. The code ‘(p q r: Prop)’ introduces three new variables, which are Propositions (statements which can be true or false). The stuff after the “:” is the theorem itself. I am aware that the implication actually can be and if and only if, however that would have taken longer to do.

Now you start writing proofs in Lean using special syntax. I won’t really go into the syntax since I’m not writing a tutorial. However, if you have seen natural deduction before, then you’ll see that this is just a specially chosen syntax for natural deduction.

Discussion

I will say that Lean is quite promising. You can do a lot more in it than propositional logic. According to Kevin Buzzard, he and some students formalized the definition of a scheme in Lean. Besides that, the ‘standard library’ contains a huge amount of math like the theory of groups, rings, and vector spaces. The fact that I was even able to write a proof that Lean verified is already a feat in itself, since I gave up on the other systems long ago.

I cannot even imagine how one could write a program like Lean. It is an incredible accomplishment. If I spent a few hours every day on Lean (and I might try…), I feel like I could get to the point where I could start proving some basic stuff in Lean like “if $x^2$ is the identity for every x in a group $G$ then $G$ is abelian”. In fact, I have written down a proof like that in natural deduction before so I know I could do it in Lean if I learned how to use it a little better.

From my general feeling, I think that I could prove even more complicated things, like the Sylow theorem in group theory or the fact that every finite field has $p^k$ elements for some prime $p$ and integer $k\geq 1$. It would probably take me a few months or more to get there. Other people have already done way cooler things than that.

I feel like it would take a very long time to figure out how to at least formalize the statements of the theorems in my papers, and some of them would certainly be harder than others. Maybe two years if I did nothing else?

That being said, Lean also needs a lot of work as a piece of software if it is to be adopted by typical mathematicians. It needs to be painless to install and use. It should not require any knowledge of the command line or git. It needs a manual for mathematicians that explains how to use it, without necessarily explaining how it works. (Did you notice that you need to know nothing about types to start out with natural deduction proofs in propositional logic?) Right now, Lean is not ready to break into the mathematical world as a useful tool. But there is rapid development, and I really hope it gets to that stage one day.

Leave a comment

Fields marked with * are required. LaTeX snippets may be entered by surrounding them with single dollar signs. Use double dollar signs for display equations.