M40001/M40009 example sheets and other things in Lean.

M40001/M40009 is the "introduction to proof" course in the maths department at Imperial College London. In the 2020 directory I am currently putting the 2020 example sheets and some other little Lean files demonstrating things from the course.

How to try the example sheets in Lean

You have two options: (1) use Lean online or (2) install it onto your computer.

(1) : use Lean online.

Here are the problem sheets for October 2020:

Sheet 1.

Sheet 2.

Sheet 3.

Sheet 4.

(2) Download the project and try the example sheets on your own computer

This only works if you have the Leanprover community tools installed; these tools will give you a fully working Lean and mathlib on your computer.

Once you have that, then fire up the command line, change to the directory where you keep your Lean projects, and type this:

leanproject get ImperialCollegeLondon/M40001_lean

Then open the project in VS Code e.g. by selecting File -> Open Folder and then selecting the M40001_lean directory. Then look in the src/2020/problem_sheets directory for this year's problem sheets, and you can look at other Lean files in the 2020 directory too, such as the ones I've been using in the 2020 videos.