Formalising mathematics. A TCC course, Jan-Mar 2021.


Thursdays 1600-1800, Teams, starts Thursday 21st Jan 2021, last lecture 11th March 2021.


If you're at Bath, Bristol, Imperial, Oxford or Warwick then you can register for the course; instructions are on the TCC website. If you are not, but are still interested, then I will be putting material up on this website and discussing it on Thursday evenings on the Xena project Discord server. [Note that we have regular Thursday evening meetings on Discord, and they're happening right now. Maths undergraduates and PhD students welcome. Get in touch with me (briefly explaining who you are) if you want an invite.]

The course


This is a course about learning to write mathematical proofs on a computer. We will be using a computer proof checker called Lean, free open source software written by Microsoft Research which runs on all major operating systems. We will be using Lean 3 and its maths library mathlib. Lean turns a proof into a dynamic document, rather like Bret Victor's explorable explanations but in the technical domain of pure mathematics. The idea of turning a proof into a dynamic document has potential for use in teaching, outreach and research in mathematics, although these things will not be explored in the course. The course will be focussing on the core skill of learning how to do undergraduate and MSc level mathematics in Lean.

We will start off with simple undergraduate level proofs, such as: defining the complex numbers and proving they are a field, or proving that partitions are the same as equivalence relations. Once we have the hang of the basics, we will move on to MSc level mathematics, working with one or more of the following ideas: schemes, local rings and local fields, cohomology theories, or anything else the audience is interested in.


If you need a grade for this course then your task is to write a project of your own, in Lean, on some mathematics which interests you. If you do that, you'll pass. If you want a distinction then your task is to get some of your own work accepted into Lean's maths library mathlib. Here are some examples of things we don't have right now in the library, but be warned, things move quickly.


We will be learning by doing. I will start each two hour session with a brief overview of the material we'll be covering, and then we will spend the rest of the session working in small groups (or individually if you prefer), filling in proofs in the digital problem sheets which I will prepare beforehand.


There are no mathematical prerequisites, beyond having a solid working knowledge of undergraduate level mathematics.

As for preparation, I would recommend taking a look at the natural number game. If you like it, and are interested in seeing more pure mathematics being done in this way, you might like the course. The work in progress Mathematics In Lean will be updated over the next few months. If you are interested in learning about type theory as a foundation for mathematics, there is also Theorem Proving In Lean, but don't be fooled by the name: this is a book which is much more geared towards computer scientists.

Before starting the course, you should install Lean. This is still a lot more painful than it should be -- be warned. You will need to type stuff on a command line. If you have problems, then please please first carefully read the installation instructions for your operating system, available at that link. If this doesn't help, ask in the #new members stream on the Lean Zulip chat (real names preferred, be nice, this is a research chat room for focussed on-topic chat about Lean).

The course material will be distributed as a Lean project. Here is an example of a Lean project working through the proof that the complex numbers are a field. A typical session in the course will involve working on a project like that (indeed, we may well be using this project for one of the sessions).