The Xena project.
The Xena project meets on Thursday evenings during term time in the MLC. We typically talk about undergraduate level maths, and type some of it up into Lean. We're building a library of undergraduate level pure maths -- me, a bunch of undergraduates at Imperial, and a small but growing community of other people from around the world. We now have a whole bunch of algebra and topology (we have most of M2PM5 and a bunch of 3rd year algebra and group theory and also much of the 4th year commutative algebra course), but we are lagging behind with analysis: we have pretty much all of M1F and we're working hard on M1P1 but we haven't even typed up a proof that the derivative of sine is cosine yet.
Now we're later on in the academic year, most people who are interested have Lean installed on their own laptop. But it is not impossible to get Lean running on the MLC machines -- see if anything here helps.
Sign up to the mailing list (for Imperial people) for local information about what's happening on Thursday nights.
I'm a complete beginner -- how do I start?
Over the summer I am going to write a whole bunch of teaching material for 1st year undergraduate mathematicians who want to learn Lean. The current state of what I have is sufficiently disorganised that it doesn't even have its own site or title page. The project is on hold at the minute but I would like to have it in some sort of shape by October 2019 when the new first years come in. Until then, here are some relevant links which may or may not help.
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.