I am running a summer project with some students. I’ve sort-of lost count of how many; I think that around 25 people expressed an interest, but some didn’t start yet. In practice we seem to get around 10-15 people coming every day. I show up on Mondays, Wednesdays and Thursdays, and I think some of the students show up on Tuesdays and Fridays too.

Students can just do anything they want, in Lean. Some students seem to be learning courses which they’re taking next year, some are going through courses they learnt this year, and so on. People tend to be working through example sheets. Some people are getting good quickly. Others are finding it harder. I know from experience (watching people learn) that even if you find it tough initially, things might fall into place later. I seem to spend my entire day answering questions. I absolutely love it.

The project has been running for two and a half weeks. Students have done elementary number theory, elementary complex analysis, group theory, finite-dimensional vector spaces, determinants, some homotopy theory, and some wackier stuff — some of the theory of dots and boxes, and a formalisation of geometry a la Euclid (or more precisely a la Tarski). Formalising problem sheet questions is a popular option. You can see what people are doing here on github. Random people come along — not all Imperial undergraduates. I’ve had two schoolkids coming along, and a Cambridge undergraduate is a regular attendee. Chris Hughes has been immensely helpful, supporting many of the other students, and I’d like to thank him personally here. Others are beginning to become helpful too. I am surprised at how quickly some people are learning. I was scared that two weeks in I’d still be telling people how to install Lean and mathlib, but we have moved well beyond that now.

Some of the mathematics above might sound easy, but there is a whole bunch of basic mathematics still missing from mathlib (theory of finite-dimensional vector spaces and matrices and basic theory of differentiable functions being two notable examples) and I wonder if whether by the end of this we will be in a position to offer some stuff to mathlib. We nearly have the fundamental group of a topological space, and I am pretty sure that we’ll have a bunch more topological stuff soon.

Another cool thing that’s happening is that a bunch of Imperial’s undergraduate example sheets are being formalised. When I was an undergraduate we were just at the point where many lecturers gave out problem sheets which were hand-written or had been typed on a typewriter and then photocopied — but a few were giving out example sheets which had been written in TeX. I wonder whether a similar sort of thing is happening now. The funny thing is that it was the lecturers writing the TeX sheets, whereas this time around it’s the students formalising the example sheets.

I don’t really know where all this is going but somehow I feel like I’m seeing more and more evidence that mathematics undergraduates are able to learn how to use this software. I think the fact that we meet together as a team is really important. I spend a lot of my time answering questions (and occasionally asking them). I had to learn Lean by myself with just the Lean chat to help me — it’s far more efficient to learn as a team. I should make sure that I have a good strategy for teaching the new first years come October. I really should get back to writing my book on Lean for mathematicians, but there are so many other things which need doing. If the students can teach each other then the need to write it becomes, temporarily at least, less pressing.