# The Lean Theorem Prover

Some time ago I heard about the Lean theorem prover. I think it was before I interned at Microsoft Research. While I was there, someone mentioned it and its online tutorial. A couple weeks back I stumbled again over the Lean tutorial. This time I actually tried it. It’s cool.

Compared to other proof assistants and dependently typed languages it is very approachable. The tutorial does not make too many assumptions. Most importantly, there is a code editor and a running Lean process right there in the browser. No fighting cabal or installing proof general to try things.

So I worked through the tutorial, which has exercises! As with most things, I did not really have a reason. I did it for the fun of it.

This week, Brian McKenna asked on Twitter (presumably as an exercise) for a function that is both idempotent and an involution.

Idempotent: f(f(x)) = f(x)

Involution: f(f(x)) = xFind functions with either property. How many functions can you find which have both?

There is only one function with both properties: the identity function.

He later linked to proofs in Idris and Coq. I thought that would make a nice exercise in Lean. It is not exactly my problem, but, unlike exercises in the tutorial, it is also not explicitly positioned as a Lean exercise. There were solutions to take inspiration from, but my own ended up being quite different.

```
open function
lemma ideminvoid (A : Type)
(f : A -> A)
(f_idem : forall x, f (f x) = f x)
(f_invo : forall x, f (f x) = x)
: forall x, f x = id x :=
take x, calc f x = f (f x) : f_idem
... = x : f_invo
... = id x : rfl
```

I like the `calc`

part of the proof.
It reads very much like a proof on a whiteboard:
*f*(*x*) = *f*(*f*(*x*)), because *f* is idempotent; *f*(*f*(*x*)) = *x*, because *f* is an involution; *x* = *i**d*(*x*), because `rfl`

, which stands for “just evaluate both sides and see that they are the same thing”, in this case, we just use the definition of `id`

.

Unfortunately, the tool support for doing actual proofs (as opposed to doing the tutorial) is a bit “meh” compared to Agda, Idris, and Coq. Lean has an Emacs mode, but it’s not great. I also don’t quite understand why they don’t use proof general. To be fair, it’s a very young project.

Anyways, this is what a proof (by a complete beginner) in Lean looks like.