I have just spent an exhilarating week in the company of a whole bunch of mathematicians, a fair few of whom are serious professors from prestigious universities, all of us learning how to use Lean to do mathematics ranging from basic logic to category theory and differential geometry.
Why? Because I’ve been at Lean for the Curious Mathematician 2020, an online meeting organised by Johan Commelin and Patrick Massot. It was like no other conference I’ve ever been to. On a typical day there were three “sessions”. A session was typically two hours long, and consisted of a mathematician who knows how to use Lean giving a 15 to 30 minute Zoom talk introducing a part of Lean’s maths library mathlib, and then the audience splitting up into breakout rooms of between 5 and 10 people, with one expert per room, and working on the exercises which the speaker had prepared. People could ask questions to each other or to the experts whenever they were stuck. A few years ago I would never have guessed that in 2020 I would have a Cambridge professor of number theory asking me for help in proving that the standard basis of 
What is even better is that everything was recorded, so if you missed LftCM 2020, you can still join in. All the talks are up on a LftCM 2020 playlist on the Leanprover community YouTube site, and all of the exercises are available at the LftCM 2020 GitHub repository. If you have installed leanproject by following the instructions on the Leanprover Community website then all you have to do is to type
leanproject get lftcm2020and then, using VS Code, open the lftcm2020 directory which just appeared on your computer. You’ll see all the exercises, and all the solutions. Furthermore, you have easy access to the very same experts who wrote the exercises because they all hang out on the Lean Zulip chat, and the #new members stream is dedicated to beginner questions. I will be live streaming my way through some of the exercises over the next few weeks on the Xena Project Discord server; I monitor the chat on most days, but aim to spend every Tuesday and Thursday on the server throughout July and August. If you’re a undergraduate mathematician, even if you’re a complete Lean beginner, you’re very welcome to join us. A good time to join us is Thursday evening UK time; there are often a whole bunch of us there then.
What did we learn?
One thing we learnt was that technology like Zoom works very well for a workshop of this nature. For a beginner, Lean’s error messages are very intimidating. But if a beginner shares their screen on Zoom so that an expert can read the error, then the expert often immediately knows what is wrong.
Something else we learnt was that a very good way to teach mathematicians how to use Lean is to give them a whole ton of exercises involving doing mathematics which they already understand conceptually, and asking them to attempt them in Lean. In some sense a large source of exercises corresponding to interesting mathematics is something which, before now, had been lacking in the Lean ecosystem. There is the very wonderful Theorem Proving In Lean, the book I read when learning Lean, but it does not talk about Lean’s mathematics library at all and focuses more on things like Lean’s underlying type system. I have always thought of it as more of a book for computer scientists. Jeremy Avigad, one of the authors of Theorem Proving In Lean, is currently working with Patrick Massot, Rob Lewis and myself on a new book, Mathematics In Lean (a book which can be read and run entirely within VS Code; read the instructions in chapter 1 on how to interact with it in this way). But this book is not yet finished. The book does not come with videos — Jeremy is writing words to explain how things work. The LftCM GitHub repository goes right to the point: every file, after a brief introduction, goes straight onto exercises, the vast majority of which can be solved in tactic mode, so it is a very natural continuation for anyone who has played the natural number game. If you don’t understand something in the file, you can watch the corresponding video and see if this helps. I will be very interested in seeing whether mathematicians find the repository a useful asset and I am almost certain that they will.
We learnt that Scott Morrison’s tireless efforts to teach both Lean and the Leanprover community category theory have now gone as far as giving us a whole host of accessible exercises, together with hints!
We learnt that smart people can pick up Lean very quickly. It was very interesting watching Sophie Morel learning to use the system, and seeing her assimilating more and more concepts as the week went on; I was especially interested in watching her learn a new trick to prove a theorem and then, instead of immediately moving on, playing around with her proof to understand the trick better. Although it sounds a bit ridiculous to compare a mathematician of her calibre to Kenny Lau (an Imperial undergraduate), watching her learning Lean this week reminded me very much of watching Kenny learning Lean back in 2017, when he was just a first year UG and within a few weeks of starting using Lean was formalising the theory of localisation of commutative rings. Kenny has gone on to contribute just under 20,000 lines of code to mathlib, including a lot of MSc level commutative ring theory. Sophie, many thanks for coming, and I hope you like what you saw. And Kenny, and Chris and Amelia, it was great to chat to you all this week and I am very much looking forward to working with all of you this forthcoming academic year on your Lean MSci projects.
One important thing, for me at least, that came out of the week, was that we got to see exactly the kind of problems which beginners run into. Lean is very much under development. New versions come out every few weeks of the community version of Lean, and the maths library is updated several times a day. There are many open issues on the Lean and mathlib github repositories, which are opened, dealt with, and closed. But as an experienced user it was interesting to see which ones were tripping people up. We know library_search sometimes fails because of the apply bug, and we know how to work around this. But this would completely throw beginners off. We know that nat.pow is not definitionally equal to monoid.pow and we know how to work around this. I would say that it is regarded as a low priority issue. But this week we saw people being totally confused by it. It is a reminder that we can still make Lean 3 a better system. I am not convinced by the “let’s just wait until Lean 4” argument. Johannes Hoelzl, a very experienced formaliser, told me that in his opinion porting mathlib from Lean 3 to Lean 4 whilst simultaneously refactoring it would be a bad idea. Despite the fact that I want to set up a theory of Picard groups, Ext and Tor, I should remember that the basics are still not 100% right and I can play my part in trying to make them better (beginning with that big subgroup refactoring).
I personally learnt that mathematicians do like Lean games. A couple of people asked me if it would be possible to make a filter game! I think this idea has definite potential! Until then, there’s always the max minigame, a game you can play in your browser like the natural number game and something which will eventually become part of the real number game.
I have learnt a lot this week. Watching other people using Lean is something I find very instructive, both as an educator and as a Lean user. Thank you to to all who attended, and to those who led sessions and wrote example sheets, and I very much hope to see many of you again at LftCM 2021.
Xena 