Perfectoid spaces!

Patrick Massot, Johan Commelin and I finished our definition of a perfectoid space in Lean! Patrick and Johan are professional mathematicians like me, not Imperial undergraduates, but I am sufficiently excited about the project that I couldn’t stop myself blogging about it. The home page of our project is here (check out Patrick’s graph, representing how Lean thinks about perfectoid spaces!) and the source code is here. We ultimately wrote around 12,000 lines of code in the repository itself, and Patrick wrote much more stuff on topological rings (formalising a bunch of Bourbaki Topologie Generale) which is already in Lean’s maths library.

What does this all mean? Well, one way of thinking about it, following the theme of this blog, might be: my virtual undergraduate Xena, who did not even know the definition of the complex numbers 18 months ago, now knows some really complicated things! On the other hand, that’s not because my real undergraduates taught her about this. Perfectoid spaces were discovered/invented by Peter Scholze in 2011, and used by him to prove new cases of the weight-monodromy conjecture and Langlands’ conjectures. Scholze was awarded the Fields Medal, one of the highest honours in mathematics, for this work.

But in my mind, the important thing is this. We all know, and indeed computer scientists have known for decades, that computer proof assistants like Lean are capable of working with undergraduate-level mathematics; indeed in my previous post I link to Abhimanyu Pallavi Sudhir’s solutions to last May’s M1F exam (the 1st year “introduction to proof” course which I teach at Imperial), and over the last 18 months I have blogged about many other achievements of Imperial’s undergraduates, and in particular the work of Chris Hughes and Kenny Lau formalising many proofs of results on our undergraduate curriculum and beyond. Ramon Mir’s MSc thesis formalised schemes in Lean in a robust way, and these are MSc level objects. But what I did not really feel I knew, until now, was whether Lean was capable of handling genuinely complex objects which are of actual interest to research mathematicians. Now we know that it is. In particular, I now see no theoretical obstruction stopping Tom Hales’ Formal Abstracts project from succeeding. In the long term, I believe that projects such as Hales’ have a real chance of changing the way humans do mathematics, and some chance of ultimately changing the way computers do mathematics.

It would still require many person-years of work to formally verify, for example, Scholze’s tilting correspondence for perfectoid spaces in Lean. But the crucial thing is that it would require far less work to formally state the correspondence. Here in 2019, formalising deep human proofs in computer proof verification systems is still a hugely non-trivial problem, which computers cannot do and which takes humans a very long time to do. But now I am sure that we are in a position where we can start telling computers the statements of precisely what we humans believe that we have achieved in pure mathematics. What computers can do with this information — well, that’s a question for the computer scientists. Given that so much effort has been put into search algorithms over the last 10 years, I should think that this would be a good place to start. I remember as a PhD student paging through a book on algebraic spaces desperately hoping to spot facts which would enable me to progress with my thesis. Can this process be automated in such a way as to be practical and useful to the 21st century PhD student?

The success of Hales’ project will involve a culture change amongst mathematicians. Ultimately it will rely on mathematicians formalising statements of their theorems, once their papers are accepted, and uploading the formalised statements to Hales’ database. We are not ready for this now, for several reasons. Firstly, we do not have enough mathematical objects formalised in Lean (we still don’t have manifolds [written May 2019]! But we will do soon, they are certainly on the way). And secondly, most mathematicians do not know the appropriate formal language which Lean understands. If my project to educate undergraduates to speak this language succeeds, and if Imperial students and others continue to get on board and formalise more and more mathematical objects, then I believe that progress will be inevitable. Imperial’s new mathematics curriculum launches in October and I will be pushing hard to digitise all the pure mathematics courses — definitions, theorems, proofs, example sheets, everything. After 25 years of teaching mathematics to undergraduates in the standard way, I am both surprised and excited to now be doing things in a completely different and new way.