Material from M1P1, formalised in Lean
I am writing heavily-commented Lean proofs of results from Imperial's M1P1 course, and example sheet questions. The general aim is to turn the material into a fully formalised mathematics textbook covering basic 1st year analysis.
I will be giving talks about this repository on Tuesdays 1-2 in Huxley 140 during the Spring 2019 term.
Kevin Buzzard