Lean Together 2020

I spent last week in Pittsburgh at Lean Together 2020. I felt privileged to be in the presence of Hales, Koepke and Avigad. These people are watching where Lean is going, and my impression is that they are happy. Massot, Gouëzel and Hölzl were also there, and it was very interesting to see them talking about manifolds (Patrick Massot and Sébastien Gouëzel are research mathematicians, but Johannes Hölzl is a computer scientist who now works for Apple in Munich and is formalising crypto). If someone had told Patrick 5 years ago that he would be going to a conference where (a) he would have technical discussions about the definition of a manifold and (b) give a talk about perfectoid spaces, I am not sure he would have taken them very seriously.

There were loads of great talks, and then of course there were some talks I didn’t understand at all. One person who truly made an impression on me was Ulrik Buchholtz. He taught me a lot about homotopy type theory. What I liked about him was that he had understood that whenever anyone says the word “constructive” I instantly hit the roof and start yelling that I simply do not care and neither do any of my friends, so he barely ever mentioned the concept and as a result I managed to be able to concentrate on what he was trying to tell me. He has a mathematical background, and explained his thoughts about how the univalence axiom is actually a good idea for mathematics. But honestly, first let’s think of new notation for it, because every mathematician knows that equality takes values in an impredicative Prop and that’s the end of it. I was always unhappy that Milne and Grothendieck used equality to denote canonical isomorphism, perhaps we just need a new notation for this kind of equality? Update a few hours later: Actually, on re-reading this post I realise that this is a lie. I thought Milne’s idea of using the equals symbol to denote a canonical isomorphism was a brilliant idea when I was a post-doc. The reason I’ve gone off it now is that I have no idea what a canonical isomorphism is so I can’t formalise the idea properly.

Sebastian Ullrich spoke about Lean 4! Summary: it’s going to be super-cool, notation will rock, and they even have 2 tactics! intro and assumption. I reckon you could prove with those, and who knows what else. The elephant in the room: porting mathlib to Lean 4. People were optimistic — but we don’t really know anything.

Hales and Koepke spoke about natural language. They have examples of text which sounds like normal English mathematical text and can be read by their Haskell program and turned into some kind of tree data structure. The task now is to turn that data structure into valid Lean code. I guess Lean 4 will be the thing to target.

Cyril Cohen talked about how to make a big library of data structures (like the theory of groups, rings, fields, totally ordered monoids etc, all at once). He was using Coq but I am sure that we have things to learn from those guys.

Reid Barton raised what looked to me like a straightforward maths question about semialgebraic subsets of , and then noted that it was super-hard to prove in Lean. He says we need to write a new tactic to prove it.

Neil Strickland raised some very important points in his talk, regarding scalability of the mathlib project. I am pretty sure that several of them still have not been dealt with.

Manuel Eberl showed us all how much better Isabelle is than Lean at analysis, and then Fabien Immler showed us again. Is this because analysis is hard to do in dependent type theory? I don’t think so, because the Coq people are also pretty good at analysis. We are just behind.

Sylvie Boldo gave a wonderful talk about Lebesgue integration in Coq. Sylvie — it was a pleasure to meet you. Sylvie is one of the people behind the Coquelicot project. What can Lean learn from this project?

On Wednesday, we had four talks by people using SMT or SAT solvers in different ways. I was worried that I would find these talks incomprehensible because I really don’t know anything about SAT solvers, but all of them — Lsitsa, Keller, Heule and Ebner — were really enjoyable. Gabriel Ebner unveiled a hammer for Lean! I’m voting Mjölnir by the way.

Mario Carneiro talked about metamath 0. I wish I could say more about his work, but it is too foundational for me to understand it properly. All I know is that we had a proof of Dirichlet’s theorem on primes in an AP in metamath and then Mario pressed a button and we had one in Lean, and it had been written by a computer and was incomprehensible. Scary?

Markus Rabe talked about Google’s dream to build a mathematician. They want to write code that reads ArXiv and spits out some kind of tree data structure. They want to read human language. Hales and Koepke are offering an alternative — they suggest that, right now, humans will have to change (i.e. learn) if they want to communicate mathematics to computers themselves.

Finally, Imperial undergraduates Chris Hughes, Amelia Livingston and Jean Lo did me proud, with intelligent comments and questions.

To everyone I saw there, and in particular to the organisers Jeremy Avigad and Rob Lewis, and also to Mary Grace Joseph, thank you very much for an extremely enjoyable conference.

Advertisement