Note that this course was in Lean 3 which is now out of date (end of life). In December 2023 I will be translating this material into Lean 4.
This is the repository for Kevin Buzzard's 2023 course on formalising mathmatics in the Lean theorem prover. The course ran from January to March 2023.
If you have Lean 3 and the community tools installed in your computer, then it's just a matter of typing
leanproject get ImperialCollegeLondon/formalising-mathematics-2023
into the command line. Instructions for installing Lean 3 and the relevant tools are here.
Whilst installing Lean and this project locally is the recommended way to do this course, if you have an account at Github you can play online using Gitpod (wait a minute or two for everything to download and set up). Briefly: when everything's finished downloading, open up the src directory on the left and then you should see the relevant files.
The course notes are here. They are a work in progress, and will grow in parallel with this repo over the period Jan to March 2023.