So, what’s been happening? Well, the Lean 4 developers told us in mid-June that Lean 4 would be released at “the end of the summer“. And on Monday Lean 4 got released! The corollary is that it’s the end of the summer now, so it must finally be time to talk about the summer projects, and some of the things which happened since then.
Summer projects
In stark contrast to the 2018 Lean summer projects, the 2020 projects all happened online, on Discord. I had far less control of what was going on, and (something which I rather liked) I ended up working with a bunch of people, some of whom I didn’t know the real name, race or gender of. I say I ended up working with them — what happened in practice was that they worked with each other. A community was born, people did Lean stuff. People did other stuff too. The community still exists. I didn’t really expect that. Undergraduate mathematicians welcome. So, what got done?
Harun Khan proved that 144 was the largest square in the Fibonacci sequence in Lean, following an ingenious argument of Cohn from the ’60s. As far as I know this result has never been formalised.
Xiang Li formalised a crazy construction of the reals directly from the integers, called the Eudoxus reals. The idea is that the reals are equivalence classes of almost-linear maps from the integers to the integers (a function 
Elizabeth Sun figured out which natural numbers were the sum of two squares. It’s great to see some basic number theory being done in Lean. I am a number theorist but for some reason a lot of my Lean work is in commutative algebra rather than the elementary stuff. Thank you Elizabeth and Harun for flying the number theory flag 🙂
James Arthur proved some theorems about some kind of twisted variants of sine and cosine. James is an undergraduate at Exeter and is currently in charge of marketing down there 😉 Thanks James.
People learnt about foundations. James Palmer, an undergraduate at Warwick, ended up writing an essay on it. Foundations are not something I know much about, but James is a maths/philosophy student so had a particular interest in it.
People made games. Kendall Frey made a Rubiks cube (although he’s not an undergraduate); Markus Himmel made formally verified Sudoku, and more recently Angela Li has made a tower of Hanoi. All these things are possible because of Ed Ayers’ widgets, part of Ed’s Cambridge university PhD thesis. Angela is now working on a 15 puzzle and thinking about “loopy” and other games from Simon Tatham’s puzzle game collection.
The summer has dragged on. People keep making stuff. Alena Gusakov and Bhavik Mehta worked hard on graph theory over the summer, initially formalising some of the problem sheets from the graph theory course Alena had attended, and now this work has culminated in a formal proof of Hall’s Marriage Theorem that Alena has put together with Bhavik Mehta and Kyle Miller! Alena gave a talk on that at Lean Together 2021 — more of that in the next post.
MSc projects
There was some sort of blurring between work done over the summer and work which is now becoming MSc projects. Chris Hughes made a group theory tactic! Given a collection of hypotheses, the tactic will try and prove another one. For example if 
All this has been a really positive change to my work life. For 20 years I’ve supervised MSc/MSci students in the maths department and many of the projects have been of the form “here’s a Springer GTM; now rephrase the relevant chapters”. I have grown tired of such projects. My colleague Toby Gee has started to give students research papers to read instead, which is brave, but still ultimately the results are a student giving an exposition of something which is there already. I now have students who are not only learning the material but also formalising it in Lean, and some of this stuff ultimately makes it into mathlib. My previous students have formalised schemes, group cohomology, and transcendence of 
Undergraduate/PG teaching
I spent September trying to learn how to teach online. I made lectures for my undergraduate course, some of them cheekily using Lean. But Lean is not a compulsory part of my course; I do not think I really have the resources to teach almost 300 students how to use some complicated software; I have to rely on the fact that students will get interested and become engaged. In the introductory course, I teach the students about sets, functions and equivalence relations, and then Marie-Amélie Lawn teaches them about how to build the naturals and the reals from scratch in an axiomatic way. A lot of this material is very Lean-friendly. Welcome to the new Imperial members of the Xena community — Aksel, Jack, Deepro, Deniz, Jia, Archie, and all the other new 1st years who came along and whose names I’ve now forgotten. These kids show up on Thursday evenings on the Discord and we work through undergraduate problem sheets together. Is this good for them? Is it teaching them mathematics in a new way? Is it making them learn better, or understand the material better? I don’t know. Maybe! Is it fun? Yes. Does it change the way these undergraduates think about mathematics? Yes. I am convinced it makes them think more clearly. Students who engage with Lean seem to be more careful about their logic, and more careful about pointing out special cases. This can’t be a bad thing. But is this because they’re using Lean, or are they drawn to Lean because they are already the kind of people who think like that? I don’t know.
Should I make Lean a compulsory part of my 1st year undergraduate course? I am not convinced. People did not come to Imperial to do mathematics in a computer proof system. Some undergraduates have no interest in using computers at all. Athina Thoma, an education expert, told me that perhaps it is difficult for a student to learn new mathematics and to learn Lean at the same time. I think this is a very pertinent comment. So why do I even put time into this optional component of my course? Because I think it is time that this area begins to grow, possibly in ways I’ve not thought of yet, and the best way to make it grow is to make sure that a bunch of smart young people know about it. This is the motivation behind the Xena project. Once mathematicians can use this software, they’ll figure out interesting things to do with it. The killer apps will come.
As a reaction to Athina’s comment, I thought it might be interesting to teach Lean to people who did know the mathematics already. And so this term I am teaching a graduate course which will deal with undergraduate mathematics! As part of the Imperial/Oxford/Bath/Bristol/Warwick EPSRC Taught Course Centre, I am teaching a course on formalising mathematics this coming term! The course will comprise 8 two-hour workshops, where I get PhD students to think about stuff they understand well and to see if they understand it well enough to convince Lean that they do. Introductory lectures will be on things like equivalence relations and basic group theory; we will later move on to harder stuff (possibly guided by interests of the audience). Current ideas for what we will do in the last couple of workshops: some algebraic geometry, condensed sets, commutative algebra? We’ll see.
Oh — talking of EPSRC — they gave me a New Horizons grant! Job ad for digitising the Langlands program is out next week 😀
Xena 