Formalising Mathematics
A handbook for mathematicians. Written by Kevin Buzzard, for his Formalising Mathematics course. Thanks as ever to Imperial College London.
Note
This document is currently under active development. It is being written during the period of January to March 2023 as part of an undergraduate course for mathematicians at Imperial College London. It’s online even though it’s currently incomplete, so that the students can access it. It will be stabilising by April 2023.
This document is written for people with some mathematical experience (e.g., people in the final year of an undergraduate mathematics degree). Its aim is to show such people how to formalise mathematics in the Lean theorem prover. We make extensive use of Lean’s mathematical library mathlib. Right now this document covers Lean 3; when mathlib has been ported to Lean 4 I will rewrite this document to cover Lean 4. My current hope is that in January 2024 we will be using Lean 4 for this course; but in 2023 we’re using Lean 3.
If you’re new here, start at the introduction. The mathematics is all in Part A.
Here’s a link to the repository for this course containing all the code. In 2022 we were still in the pandemic so I made some videos which may still be of some use (although they refer to a slightly different reordered repository). Here’s a link to the YouTube playlist where I work through the 2022 problem sheets and discuss techniques.
Here is a pdf of this document.