Lean Library currently studying for a degree at Imperial College
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 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
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.
Some of the lean files are in a library called Xena. One could imagine Xena as currently studying mathematics at Imperial College London. To find out more about her, you could check our her blog at
https://xenaproject.wordpress.com/
Vague long term goals:
-
Get many of the example sheet questions and solutions typed up in Lean and into a Lean problem bank, hosted here.
-
Type up Lean versions of all the theorems and proofs in the course.
-
Make an "M1F tactic" which attempts M1F problem sheet questions.