It's Thursday 8th November 2018, I'm in the MLC, and want to use Lean! What do I do!
ICT sort-of fixed it!
1) Start VS Code (via the software hub)
2) File -> Open Folder
3) Navigate to C:\xena\my_project and then "select folder"
4) Under MY_PROJECT in VS Code, open up "src" and click on "test.lean".
5) If it doesn't work, let me know and I'll update these!
One solution is to use Lean at CoCalc.com. Go to www.cocalc.com, create an account (use your Imperial email address), and then send me an email (I'm buzzard@imperial) telling me the email address you used. I will enrol you to the M1F class on cocalc and then the red cocalc warning exclamation mark will disappear and you should be able to use Lean fine.
Alternatively, install Lean yourself on a machine in the MLC. [NB updated 8th Nov -- Lean is now installed again on the MLC machines, in C:\xena , so you don't need to do this now]. Installation takes about 5 minutes. Follow the instructions here.
Sign up to the mailing list (for Imperial people) for local information about what's happening on Thursday nights.
I'm in the MLC -- what do I do now?
Log into a computer and launch Visual Studio Code via the software hub, then try looking at the book below
Let's do M1F stuff on a computer.
I'm slowly writing some kind of book, or instruction manual or whatever. My goal is to teach undergraduate mathematicians how to use the formal proof verification system Lean by showing people how to solve the example sheets for my course, and other questions which come up over the term.
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.
The Equivalence Relation Challenge
The challenge as I originally posted it is here
The book is sufficiently disorganised that it doesn't even have its own page. But here are some relevant pages from the book.
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
You might like my blog and in particular if you are a 1st year undergraduate maybe you would like an introduction to the natural numbers -- this post was very popular last year.
I learnt a lot about Lean from reading theorem proving in Lean. This is a book which mathematicians can try to read, and of course it has the advantage that it's finished whereas my book is all over the place. However many of the examples in that book are more geared towards computer science.
Finally, you can come and hang out on Zulip and ask questions there. The #new members stream is specifically for people with basic questions about Lean.