Over the last couple of years I have become more and more interested in the idea that soon computers will be helping humans to do mathematics research — not by crunching millions of examples, but actually filling in proofs of lemmas, and offering powerful search tools for theorems. I want to help this to happen. I have met serious computer scientists who believe that computers will be better at maths than humans by 2030. I am not one of those people, however I believe that by 2030, pure maths researchers will be using computers in new ways — to help them find proofs.
To make this dream become a reality, we need to get more computer scientists in mathematics departments, so that computer scientists can begin to understand the kind of mathematics which is done by human researchers. And to make that happen, we need to make mathematicians notice the phenomenal proof verification tools being developed by computer scientists, tools which most mathematicians are completely unaware of and, in my experience, are not yet particularly interested in.
My proposal is to change mathematics departments from the bottom up, and start with the undergraduates. The Xena Project is about showing undergraduates how to use formal proof verification software to manipulate theorems and problems which show up in their undergraduate courses. I have integrated one piece of software — Lean — into my “introduction to proof” course at Imperial College London, and results have been very positive. Several Imperial undergraduates have made contributions to Lean’s maths library, and Imperial undergraduates now sometimes use Lean in their undergraduate projects . My blog is mostly undergraduate-focussed and most of my posts are written with mathematics undergraduates as the target audience. Two experts in mathematics education — Athina Thoma and Paola Iannone — are currently trying to figure out whether my approach changes the way undergraduates think about proof. I am eagerly awaiting their results.
Tom Hales is running the Formal Abstracts project, and his ultimate aims are similar, although his methods are different, which is great. As far as I can see, for Hales’ project to succeed, we need, as soon as possible, to define many standard mathematical objects in Lean. Part of my motivation is to train undergraduates to help with this task, which I perceive as achievable. Peter Scholze got a Fields Medal for discovering perfectoid spaces and applying them to prove profound results in the Langlands philosophy. Lean can handle perfectoid spaces so as far as I can see this means it must be able to handle any mathematical object we throw at it.
As well as introducing mathematicians to formal proof verification software, another aim of the project is to digitise the curriculum . Formalising the theorems and proofs in Imperial’s undergraduate mathematics curriculum will have many benefits — no errors or ambiguities in proofs, no errors or ambiguities on example sheets, and it is an extremely natural way to start digitising all the basic objects and results which a pure mathematician knows. I am hoping that by 2025 all of Imperial’s pure mathematics courses in years 1 to 3 will be digitised. Again this seems to me to be a very achievable aim.
Finally, I am concerned about the state of pure mathematics research. More and more, results depend on theorems whose proofs are unpublished or sketchy (or even, in places, incorrect). We rely more and more on unnamed teams of experts who have a sufficiently broad overview of an area to be able to tell us with confidence which papers can be trusted. Fashions change, people desert areas, and I am genuinely scared that we are leaving a mess behind in some areas. There are some theorems whose proofs might be difficult or impossible to reconstruct in 20 years’ time. If the research is not reproducible, it is not science. Over 30 years after its announcement, the proof of the classification of finite simple groups available to the non-expert (or the formal proof verification system) still seems to rely on papers which cite papers which never appeared. Finite group theorists are currently trying to put together a self-contained complete proof of the result. Until their work is finished (and it is not yet finished), I believe that this proof is at risk of dying. The experts know how it goes — but in 20 years’ time, will there be any experts left? I regard the situation as a race against time. Will formal proof verification systems be able to help? Not at present, but who knows what the future may hold — and they are an order of magnitude more accurate, and more honest, than humans, so it’s a step in the right direction.