Summer projects 2020

I had planned to work with a bunch of Imperial College London mathematics undergraduates this summer, formalising arbitrary mathematics in Lean. I did this in 2018 and it was really good fun.

Now it looks like the College will be closed over the summer, but the students seem to still want to do it, so we’ll have to do it remotely. This means that there is now no longer a requirement that the students have to be in London (it will be less ideal than in 2018, but we have to live with this anyway). On the plus side, it means that it will be easy to slot other people in, which means that I can open it up to mathematics undergraduates anywhere in the world, in theory. So that’s my plan. We can write collaborative code on CoCalc, I can give lectures and live coding sessions on the new Xena Discord server, we can chat and hang around with world experts on Zulip, all the infrastructure is there. I have put up a preliminary page here with some details, and more is to come. The plan is to meet on Tuesdays and Thursdays, during working hours UK time, starting on Tuesday 30th June 2020, and running to Thursday 27th August.

If you are an undergraduate mathematician and want to learn how to write proofs using a computer program, and have some time over the summer, then this might be a good way to meet other people with the same interests.

Ideally students will already know a tiny amount about Lean before we start. The natural number game is one place to start. During May and June I hope to record a series of “ten minute Lean” tutorials. Currently there is only one, because I have not really worked out how to YouTube, but I will get there. There are also some basic maths Lean questions on CoCalc and a growing list of Lean kata at Codewars, and once you have installed Lean and the amazing leanproject tool you can download the tutorial project which currently contains one tutorial, but more are in the pipeline. OK so I have a lot to do. But so do you! And we have two months to do it, right?

I think I would be naive to think that I am going to end up swamped. This is in some sense pretty niche material. But people will be able to help each other, once we all get going, and I think it will be fine. My university teaches maths undergraduates how to write python and how to write LaTeX, and I don’t see any reason why they shouldn’t learn to write Lean as well — I think that doing problem sheets in Lean is a cool thing to do. I give out some of my problem sheets in Lean format nowadays, and the best thing about it is that I don’t need to mark any Lean solutions because they are guaranteed to be correct 😀

If you know any undergraduates who might be interested — pass the news on! We’re going to be formalising any kind of pure maths at all, from “do the exercises in this basic group theory book” to “formalise the basic theory of C-star algebras”, from “formalise a solution to this recreational puzzle” to “prove the fundamental theorem of Galois theory” — anything, as long as it is well-defined pure maths, is fair game. It will be interesting to learn what maths is currently hard and what is currently easy to do in Lean, and the best way to find out is by trying.

This might just look like a bit of fun, but it is really a research project. Humanity really still does not understand what the best foundational system is for doing the kind of mathematics which mathematicians do, and indeed Larry Paulson and Martin Hyland both independently told me that the best system depends on the kind of mathematics you want to do. But I now believe that this is not an acceptable answer. When I was a 3rd year undergraduate there were 12 pure mathematics courses on offer at my university, and I sat in on all 12 of them, just to see what was going on in them. They covered algebra, analysis, topology, geometry, number theory, and logic. I noticed when I was a post-doc that my subject area, algebraic number theory, used stuff taught in every single one of the courses I had seen during that year. Number theory is 2000 years old and has learnt to borrow from many other areas of mathematics. I believe that one day computers will understand the kind of mathematics that is going on in my PhD thesis, but for that to be happening we have to see it all going on in one system. I believe that projects like the one I’m describing above will show us strengths and weaknesses in Lean. If you think about it this way, failure = success, because if you decide to formalise X and then it turns out 8 weeks later that a simple looking mathematical proof turned out to be really hard to do in Lean, then actually this might be an important data point.

Advertisement