A Lean formalisation of parts of Martin Liebeck's "A concise introduction to pure mathematics".
A Xena summer project.
This is a Lean 4 project. Assuming you have already installed Lean and its supporting tools you can install this Lean project with
git clone git@github.com:ImperialCollegeLondon/M1F-explained.git
cd M1F-explained/
lake exe cache get
and then you can start the project in VS Code by typing
code .
Kevin Buzzard, Mark Zhou, Siddharth Hariharan, Katie Watson, Douhan Wang, Zhangir Azerbayev, chrt, Yuchen Wang, Xialu Zheng, Natasha Johnson, Adil Raza, Archie Browne, Faris Hafizhan Hakim, Yuming Feng.
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.