Introduction to University Mathematics (M40001/M40009) : additional Lean material

Lean is not an official part of Imperial's Introduction to University Mathematics course, but a lot of the material in Parts I and II is really nice to do in Lean.

If you are taking the course in October 2021 and you are looking to try doing some of the material in Lean then you should head on over to the 2021 page here.

For the best user experience it's worth installing Lean on your own computer. Instructions on how to install Lean and "mathlibtools", tools which will make doing mathematics in Lean 3 much easier, then head on over to the installation page on the Lean community website. Once you have done this you can just install this M40001/M40009 Lean project by firing up the command line you used to install Lean and typing

leanproject get ImperialCollegeLondon/M40001_lean