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.
Kevin
Xena 
Congratulations! This is very impressive and is a great contribution to both the Math and the Lean communities.
LikeLike
I have a comp. sci. student potentially interested in doing something as a summer project with me, and I suggested we could look at doing something in Lean. He is not a mathematician, but has done subjects of the kind where they build a virtual CPU from logic gates to writing compilers. I have some ideas of things I’d like to prove in Lean but they are, I guess, not at the level he would be comfortable with. Do you know of anything I could point him at?
LikeLike
You should just come to the lean zulip chat and ask there. I had a bunch of maths students and it was easy — I just said “choose a random thing (theorem, definition, problem sheet) from the curriculum which you liked doing or want to learn something about, and try and do it in Lean”. But there are plenty of computer scientists at the Lean chat who would be able to give you better advice.
LikeLike