The pdf example sheets for my course are here and if you are impatient and want to look at last year's course page (which has all the example sheets on) then this is here.

The Lean versions will appear in this github repository.

If you went to 342 with Dr Britnell in the problems class on 18th October 2018 then you might also be interested in this repo where we're working on question 6 of his hand-out.

Some of us are going to start work on irrational numbers -- more on this later.

To solve maths problems in Lean you need to be able to (a) access Lean and (b) know how to write Lean code. If you are at Imperial College London then Lean is installed on all the computers in the MLC and you can just run it by firing up Visual Studio Code. Alternatively Lean is also available on CoCalc and if you create an account there with your Imperial College email address and then email me, I can give you further instructions. If you are not at Imperial College then you will have to download and install Lean (and the maths library) yourself, and then clone the example sheet repository. Good luck -- it's technical. I wrote some instructions on how to install Lean on my blog.

1) stuff about propositions -- a basic introduction to Lean, which should help with M1F Sheet 1 questions 2 to 4.

2) techniques needed for sheet 1 question 1.

3) stuff about sets which will help with sheet 1 Q7