My name’s Kevin Buzzard and I’m a professor of pure mathematics at Imperial College in London, specialising in arithmetic geometry and the Langlands program, a branch of modern algebraic number theory. I believe that digitising mathematics is important, for the simple reason that digitising anything enables you to do new things with it.
Currently the computer proof systems we have are not good enough to tell mathematical researchers anything new about the p-adic Langlands program or other trendy Fields Medally things, so the top mathematical researchers tend not to be interested in them. However I am not so crazy to believe that they will never be useful to us, and the point of the Xena project is to make it happen sooner.
Young mathematicians are increasingly spending their time using computers to play games, including puzzle games. The Xena project is an attempt to show young mathematicians that essentially all of the questions which show up in their undergraduate courses in pure mathematics can be turned into levels of a computer game called Lean. Furthermore, they have a bewildering array of tools with which to solve these levels — the so-called interactive tactics. It’s like Zen Zelda.
The Xena Project is an attempt to change mathematics departments from the ground up, by teaching students new techniques. One could imagine things like formally verified course notes, which would later turn into some searchable database, and then to a tool which attempts example sheet questions by applying theorems from the course. We do not really understand what we will be able to do in the future — we’ll have to wait and see. But the more people are familar with the software, the sooner interesting things will happen.
There is a research aspect to all of this too. Firstly, the more mathematicians use these provers, the more the computer science community will begin to understand what mathematics actually is in practice in mathematics departments. No available system currently has all of an undergraduate pure mathematics degree, so undergraduates can even contribute to research projects. Over ten Imperial maths undergraduates have contributed to Lean’s maths library, and there are plenty of students at other universities in the UK and beyond who have also got involved.
Imperial undergraduates now sometimes use Lean in their undergraduate projects. Here is a link where you can see the kinds of things which young mathematicians are doing in Lean.
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.
In the near future I believe that maybe computers will be able to help humans like myself (an arithmetic geometer) to do mathematics research, by filling in proofs of lemmas, and offering powerful search tools for theorems. I believe there is a clear path towards prototypes of such machines, but there is still a huge amount of work to do before this happens, and one consequence of teaching young mathematicians to be Lean users is that ultimately it might be these people who make the machines.
Xena 