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 2022 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 2022.
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.
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, and here’s a link to the YouTube playlist where I work through the problem sheets and discuss techniques.
Here is a pdf of this document.