The work in this repo has been ported to Lean 4 and is now ongoing at this Lean 4 repo.
A Lean formalisation of parts of Martin Liebeck's "A concise introduction to pure mathematics".
A Xena summer project.
This is a Lean 3 project. Assuming you have already installed Lean and its supporting tools you can install this Lean project with
leanproject get ImperialCollegeLondon/m1fexplained
Kevin Buzzard, Mark Zhou, Siddharth Hariharan, Katie Watson, Douhan Wang, Zhangir Azerbayev, chrt, Yuchen Wang, Xialu Zheng, Natasha Johnson.
Right now, feel free to make pull requests adding either statements of, or solutions to, the exercises. Feel free to also write in English in the comments what the exercises say.