M1F, explained

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.