Material from M1P1, formalised in Lean
I am writing heavily-commented Lean proofs of results from the M1P1 course, and example sheet questions.
I will develop this repository on Tuesdays 1-2 in Huxley 140 during the Spring 2019 term.
Kevin Buzzard