Formalising Mathematics
A handbook for mathematicians. Written by Kevin Buzzard, for his Formalising Mathematics course. Thanks to Imperial College London for letting the course happen.
Note
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.
If you’re new here, start at the introduction.
Here’s a link to the repository for this course containing all the code.
Overview of these notes
Part A is somehow an abortive attempt to explain more information about various sections in the course Lean repository, although for most of the sections I just write comments directly in the Lean code. It can thus be regarded as a failed experiment, although I leave the information here on the basis that it might still be useful.
Part B is a collection of notes on various more “computer-sciency” topics which I wrote for the course. They are written with mathematicians in mind rather than computer scientists.
Part C is a list of many basic tactics including documentation and examples. I am not totally happy with the state of tactic documentation in Lean 4, so hopefully this is of some use to people trying to figure out how to use tactics in Lean 4.
Here is a pdf of this document.