I visited Microsoft Research in September and then came back to the chaos of a new academic year, a new cohort, and a new curriculum. Sorry it has taken me so long to write this post.
So at Microsoft I spent most of my time talking to Leo De Moura and Daniel Selsam. Leo is the main Lean developer, currently working very hard on Lean 4. Daniel is working on the IMO Grand Challenge. 30 years ago I think that was manifestly clear that no computer theorem prover from that time could ever get a gold medal on the IMO. Daniel is using Lean 4 and investigating how it could be integrated with AI. Daniel is adamant that he wants nothing less than a gold. My attitude was “if a computer manages to solve just one IMO problem by itself, by running the
IMO tactic on a formalised version of the question, then that would already be pretty awesome. But take a look at Machine Proofs In Geometry by Chou, Gao and Zhang and then look at these talk slides — computer scientists are developing tools which solve geometry problems, and remember that IMO geometry, unlike number theory, is a decidable domain (Tarski showed that basically bashing out the coordinates always works). Daniel grilled me about inequalities and I don’t think I did very well — I was never any good at those (or, for that matter, at the geometry questions). Fortunately for Daniel, Reid Barton visited Microsoft Research a few weeks later.
And I finally got to meet Leo properly. One interesting thing about Leo is that whilst he is giving me code which enables me to express all my mathematical ideas completely rigorously, Leo himself has no interest in learning any of the advanced mathematics which we have been doing in Lean. Leo is trying to write a programming language which runs on a certain kind of dependent type theory and which will compute quickly in a way which is provably bug-free. For example I’m sure Leo would be very interested in talking to people who wanted to use Lean to develop a bug-free operating system for a computer.
Having said that, I’m sure that my visit would have been a great opportunity to learn something about the Lean source code, to take a look at all those C++ files and try and find out what the computer actually does with its C++ objects when I’m telling it to apply induction. But I have no idea about C++ and I don’t think we talked about the code at all, even though he wrote most of it.
But Leo and I actually had loads of other things to say to each other. I gave a talk, he asked me what mathematicians needed and I told him some problems we’d had with getting our ideas into Lean. The boundary of my interest in the Lean Theorem Prover is usually the Tedious Implementation Issue . For example, there are about three ways of doing homomorphisms of rings in Lean, and they’re all what I as a mathematician would call the same. On the other hand, the computer scientists have technical conversations on the Lean chat about which implementation will suit our needs best, now they are beginning to understand them better. This is a key point. We had a ring morphism and an -module and we wanted to consider it as an -module. They said “Oh, we didn’t know you needed that functionality, and this is unfortunate because we’ve set it up so that modules could only be modules over one ring, and changing it will result in having to create a new copy of the module, which wouldn’t be very good. Hang on, we’ll fix it”. And they did, and it took Mario Carneiro a very long time to fix it, but fix it he did. And now using modules in Lean is quite similar to using modules in mathematics, as long as you know the module library. One day we’ll have automation which means you won’t even need to know the library that well, but sledgehammers in Lean are very much a work in progress right now.
What I want to do is mathematics, without ever caring about tedious implementation issues. You could say that the Xena project is trying to figure out how much these issues can be avoided. By encouraging undergraduate and PhD level mathematicians how to formalise their ideas in Lean we are getting better and better at telling computer scientists what modern mathematics looks like, and then people like Leo and others will be better informed when they are making big design decisions about how to write Lean 4. This is one of the reasons why what goes on at the Xena project is important.