It was a year ago today that I emailed Inkeri Hibbins, a wonderful administrator at Imperial College London, and asked her if she could email all the Imperial maths and joint maths/computing undergraduates and tell them about my new Thursday evening club called the Xena Project. At that time I was still struggling to prove that the real numbers 1 and 2 were distinct. But I knew that I somehow wanted to formalise a whole chunk of the undergraduate syllabus.
Fast forwards exactly one year, and somehow Lean’s mathematical library contains, as of today, a whole bunch of Imperial’s first year pure mathematics curriculum, and some of the second and third year pure curriculum too. Today the developers, which include Imperial undergraduates, announced definitions of the exponential function, and sine and cosine. These definitions represent a filling-in of one of the very last few missing pieces of the project to formalise my undergraduate course, M1F. My course is based on Martin Liebeck’s book “what is mathematics”. One of the chapters in that book talks about Euler’s formula for a convex polyhedron. I think that that’s the only chapter left of M1F. So much progress has been made. Thank you to everyone involved. M1F is running for the last time ever, this year, but something new and exciting will rise from its ashes and the Xena project will be ready for it. What is more, the Lean maths library also contains a bunch of stuff from M2PM2 like characteristic polynomials and determinants of matrices. A whole bunch of foundational work for this stuff was done by Imperial undergraduates (and Keji 😉 ) and I would like to thank all of the people who came along to the Xena project last year, particularly Chris Hughes and Kenny Lau.
And last but not least I would like to thank all of the Xena Project summer students. I made many funding decisions using random algorithms, because Lean is for everyone who is interested. I am sorry I couldn’t fund all of you. You have convinced me that this entire endeavour is worth continuing with. Here’s to a great term and hopefully I’ll see some of you on the evening of Thursday 4th at Xena.
If you’re not at Imperial but want to know how to use this material, come and ask at the Lean maths chat (Zulip : registration required, real name preferred). I’d be particularly interested to hear from other people involved in undergraduate teaching at this sort of level, or students about to start a mathematics degree.