Note: this is not a functioning Lean repository! This is simply a collection of files written by Kevin Buzzard and his students between 2017 and 2019 as we experimented with how to teach Lean parts of Imperial College's undergraduate mathematics degree.
This is a collection of files written by Kevin Buzzard and some of his students. Kevin Buzzard is the lecturer for the "M1F" course at Imperial, which is the standard introduction to proof course which runs at many UK universities. The official name of the course is "foundations of analysis" although there are other things in there too.
The M1F course was designed by Martin Liebeck and it is based on his book "A Concise Introduction to Pure Mathematics", published by Chapman & Hall.
Current student contributors in alphabetical order:
Ellen Arlt Tudor Ciurca Chris Hughes Kenny Lau Amelia Livingston Julian Wykowski
The files are mostly written in a computer language called Lean. Lean is an automated proof checker. You can find more information about Lean at
https://leanprover-community.github.io/
Basically, Lean can understand mathematics, and can check that it doesn't have any mistakes in. Most of the files here are Lean verifications of various pieces of undergraduate level mathematics.
Initially I had imagined that this project would turn into a formalisation of chunks of the undergraduate degree at Imperial College; however Lean's mathematics library mathlib ultimately turned out to fulfill this role. For more about the Xena project, which is focussed on teaching mathematicians about formalisation, see
https://xenaproject.wordpress.com/
For more about Lean's mathematics library, see https://leanprover-community.github.io/ .