M1F, Imperial undergraduates, and Lean

M1F is the “introduction to proof” course which I have taught for the last few years at Imperial College London. When I started this blog just over one and a half years ago, one of my goals was to see whether Lean could handle the solutions to an M1F exam. At the time it was pretty clear that it wasn’t ready — a random sample of M1F exams showed that most of them mentioned either the complex numbers, or functions such as the exponential, sine and cosine function. None of these were in Lean at the time.

I wrote some basic complex number code myself, and PR’ed it to the maths library; it was my first serious PR. A team led by Chris Hughes (at the time a first year) did sines and cosines and the exponential function. And now the inevitable has occurred: Abhimanyu Pallavi Sudhir, a current first year, has formalised the solutions to last year’s M1F final exam! Many thanks to Abhi — I was pretty sure this sort of thing should be accessible, but this is the proof. Apologies to Abhi for taking so long to get around to looking at his work. I believe that having concrete goals like this are a good way of driving Lean’s maths library in the direction which I want it to go in — formalising mathematics which is actually used by mathematicians. One reason I took so long to look at it was that I have been very focussed on the perfectoid project recently — but more of that in another post.

Funnily enough, one of the things in the exam which was the trickiest to do in Lean was the proof that 0.71 has no 8’s in its decimal expansion! Lean still does not have a theory of decimal expansions, although Calle Sönne and I will eventually get around to writing one (after exams). In the mean time, I wrote a definition from first principles which does the trick. Another irritating issue is the question about a set with two elements, which a mathematician can start with “WLOG the set is “. I believe you — but this actually takes a few lines to justify in Lean. Something is missing here — a transport tactic of some kind. We’ll get there one day — the computer scientists are on the case.

20 months ago, formalising the solutions to an M1F exam seemed like a dream away. I’ve already mentioned three undergraduates who were involved in one way or another in realising this dream. All this made me start wondering about which Imperial undergraduates have contributed to Lean’s maths library, and what they have done. At the top we have Chris Hughes and Kenny Lau, who have made many many contributions. Kenny made a robust theory of localisations of commutative rings, essential for our work on schemes, and Chris proved the law of quadratic reciprocity and the fundamental theorem of algebra, amongst many other achievements. Both Chris and Kenny wrote their first year projects in Lean, and Chris is now a maintainer for Lean’s maths library! But here are a whole bunch of other Imperial undergraduates who have managed to get namechecked in Lean’s maths library as well:

• Ellen Arlt (matrices)
• Sangwoo Jo (number theory)
• Guy Leroy (number theory)
• Jean Lo (analysis, irrationals, operator norms)
• Rohan Mitta (topology)
• Blair Shi (matrices)
• Abhimanyu Pallavi Sudhir (irrationals, analysis, hyperreals)
• Calle Sönne (analysis, irrationals)
• Andreas Swerdlow (algebra)

I must also mention Guillermo Barajas Ayuso, Luca Gerolla, Clara List, Amelia Livingston, Elliott Macneil, Ramon Mir and Ali Sever, all of whom wrote a substantial amount of Lean code which they did not PR; Clara on primes of the form (completely solving the problem for ), Luca on fundamental groups, Guillermo on analysis, Elliott on group theory and number theory, Amelia on group theory and Ali on Tarski’s formulation of 2d geometry. Ramon Fernandez Mir has written his MSci project in Lean! And last but not least, Keji Neri, who did a bunch of algebra over the summer with the Imperial summer students, even though he is a Cambridge undergraduate — the only one to have contributed to Lean’s maths library as far as I know. Oxford, Warwick, UCL, Bristol — where are you? Lean’s maths library is ready to digitise a huge chunk of your curriculum. Let’s do it — it will scare the grown-ups.

Finally, some news on Athina Thoma. Athina is the post-doc who has been observing the Imperial undergraduates and trying to figure out whether Lean helps them to learn proofs better. First great piece of news: she has had her contract renewed for another six months! Second great piece of news: slowly she and Paola Iannone are beginning to make sense of all the data they collected. I await with interest the paper they are writing, and the conclusions they will draw.

Advertisement