The Xena Project summer projects, 2020.
In July and August 2020 I had planned to "supervise UROP (Undergraduate Research Opportunities) students". I had planned to work with a team of undergraduate mathematicians at Imperial College London, formalising mathematics using the Lean theorem prover. I did this in 2018 and found it incredibly rewarding. Because Imperial College is closed for the foreseeable future, I now need to change my plans.
My plans now are still to work with a team of undergraduates, formalising mathematics using the Lean theorem prover, but now we will work online. Because of this, the project is now, I guess, open to anyone. Here's a link to my Lean discord server (Note added August -- the server is still running but the link has now expired). Things will get going in July but feel free to brainstorm ideas before then.
When?
I plan to devote Tuesdays and Thursdays to project supervision (10am-6pm or so, UK time), but of course students are welcome to ask questions to each other any time they like. I will give a talk on each of these days, on Tuesdays in the morning and on Thursdays in the afternoon, and will spend the rest of the time talking to people with questions. I will start on Tuesday 30th June and will run the program for 9 weeks, so will finish on Thursday 27th August. More details about where and how we'll communicate will appear later (when I've worked out the answers).
What?
The goal of your project will be to formalise some mathematics in the Lean theorem prover. Any mathematics will do. It can be some you already know (or think you know), or some you want to learn. It can be recreational or serious. It can be theorems that are already in Lean's maths library, theorems which are completely inappropriate for Lean's maths library, solutions to the problem sheets for that group theory course you liked, anything. By the end of it, you should have a repository on GitHub containing some Lean code which compiles without errors, and a brief explanation of what your code does. Here are some examples: compact unit ball, Kruskal-Katona, schemes, Sylow's theorems, but even if you don't know that kind of mathematics it's fine -- people have even formalised Olympiad problems and a whole bunch of random undergraduate level mathematics (warning: that last link is very old code from when I last did this, and it's not organised at all -- I learnt a lot from that experience, and this time we will do it better). Some random ideas for what to formalise (perhaps appropriate for 3rd year undergrads or higher) are here (although people are completely free to formalise what they want).
How?
First you need to learn how to do mathematics in Lean. You can try the natural number game, and you might also want to check out theorem proving in Lean, although the latter is quite computer-sciency.
Second, although you can goof around with the online Lean web editor, ultimately you will have to install Lean and the maths library tools onto your computer and then create a new Lean project or download the tutorial project.
You might then want to start on the Lean levels at CoCalc or Codewars, or you could try the problem sheets from M40001/M40009, my introduction to proof course at Imperial College.
Note that if you are prepared beforehand and know a bit about how Lean works, and if you already have Lean installed on your computer, then you will be able to get started on day one. Note also that more Lean tutorials for mathematicians will be appearing soon -- check out the tutorial project and Codewars because things get added all the time there.
Money?
There is no money involved, and no forms to fill in. It is completely free to join, and I can't pay you a salary. If you decide to drop out after 2 weeks, that's fine. It's completely informal, unless you officially registered via Imperial's UROP program in which case there might be money involved and you might be expected to produce something, but you'll know if this applies to you.
I'm stuck/I have a question
Ask it in the #new members stream at the Lean chat. Real full names preferred, be nice, and please try and solve your problem yourself before asking, and please don't assume that it's easy in Lean because you think it's easy in maths. Formalising is hard, you have to learn to think in a new way. If it's easy in maths, it probably *is* easy in Lean, if you're an expert...
Kevin Buzzard, last modified 9th June 2020.