About

This blog is basically documenting my attempts to learn how to do undergraduate level pure mathematics within the Lean theorem prover. It also documents my attempts to write teaching materials which will hopefully aid others to do the same, and my attempts to teach some of the undergraduates at Imperial College London to use Lean. If I can get a core bunch of keen undergraduates involved I think this might become a really fun project.

We (the undergraduates and I) will be learning by doing, and what we are doing is creating a bunch of lean files and libraries called Xena, hosted on Github. This term I am teaching an introductory course on proof called M1F, and my initial goal is to see if we can prove all of the M1F theorems and do all of the M1F example sheets in this Lean language. I have anthropomorphized the library, and I often refer to Xena as a virtual undergraduate. The reason I like this way of thinking about the project is that I think that a very natural time to type the M1F sheets and course into Lean is whilst I am teaching it, so it really does feel like I am teaching Xena M1F at the same time as I am teaching it to the undergraduates.

Kevin Buzzard