This is the repository for Kevin Buzzard's 2022 course on formalising mathmatics in the Lean theorem prover. The course ran from January to March 2022. Note: the 2023 version of the course is here.
If you have Lean 3 and the community tools installed, then it's just a matter of typing
leanproject get ImperialCollegeLondon/formalising-mathematics-2022
into the command line. Instructions for installing Lean 3 and the relevant tools are here.
The course notes are here. Note: the 2023 course notes are more up to date.
The accompanying videos are in a YouTube playlist here.