What is the Xena Project?

Note (added June 2019); this (below) is an old blog post from 2018. You should really read the updated one here but I’ve left this original one just to preserve history.

The current aims and ambitions of the Xena Project are twofold.

1) Digitise the curriculum. I would like to see the main definitions, theorems and proofs, and example sheet questions and solutions, in all of the undergraduate pure mathematics courses at Imperial College London, typed up into formal proof verification software.

2) Teach undergraduates the new way. I would like to teach mathematics undergraduates how to use formal proof verification software.

Many people have asked me why I want to do these things. Here are four reasons, in no particular order.

Reason 1: I conjecture that offering undergraduates the opportunity to type basic proofs into a computer will actually make them learn better. I am actively involved in an educational project with Athina Thoma and Paola Iannone where we aim to investigate this. Most mathematics departments in the UK teach students to use basic “calculational” software such as Python, Matlab or R. I am suggesting that we should extend this to “verificational” software such as Lean, Coq or Isabelle — whichever turns out to be the most appropriate and/or useful. I had to choose one — I chose Lean. In March 2019 we hope to have our first results and I will post something at this blog.

Reason 2: Computers are now capable of understanding and doing undergraduate level mathematics. In my mind this is a huge deal. They currently don’t do it very well. But they understand it extremely well. And I believe that it is only a matter of time before they start doing it very well. As a benchmark (or challenge), I would be interested in when we will able to get a computer program to pass the end of year exam for my first year undergraduate course. One must of course say exactly what one means by this, and there are many interpretations, some far more difficult to achieve than others. But I believe that for some interpretations of this challenge (involving, for example, a human translating the exam into a format readable by the computer), this may be just about accessible within a few years — and note that I say “pass”, not “get 100 percent”. My belief is that the media would be interested in claims that computers can pass undergraduate maths exams. More importantly, I am hoping that funding agencies will be interested. This goal is still at least several years away and might be harder than I think. However the goal of teaching a computer our entire pure mathematics curriculum is most definitely accessible, of this I am 100 percent convinced. I would like to have completely achieved digitisation of the main definitions, theorems and proofs of our curriculum, with the help of my undergraduate co-workers, within the next five to ten years.

Reason 3: It is simply blue sky research. The people who developed the CD or mp3 as a method of digitising music — if you asked them why they were doing it, do you think they would have replied “so someone can invent the iPod and Spotify”? I don’t think so. Their answers would have been vaguer, perhaps of the form that digitised music is easier to move around, costs less to store, and can be analysed in new ways. If we have a database of theorems, we’ll be able to do search, we’ll be able to suggest possible theorems to people using the software, we’ll be able to run AI on the database. What will come of any of this? I don’t know. But let’s find out. There is no time frame on this.

Reason 4: I know, and indeed all researchers in pure mathematics know, that the modern pure mathematics literature contains gaps, and some of it is wrong. I believe that most of the gaps can be filled, however I believe that some of these fillable gaps can only be filled in by a handful of experts. Similarly, the experts know which parts are wrong. I think that all of this is unsatisfactory. It acts as a barrier to learners, it creates elite clubs of people “in the know”, and there is a chance that it will lead to disaster. I would like to change the culture of mathematics, so that more and more people begin to consider formalising mathematical arguments that they learn or come up with. It will be decades before computers catch up, if they ever do. It will probably cost hundreds of millions of pounds worth of person-hours to digitise any one of the known proofs of Fermat’s Last Theorem, and once digitised, these proofs will need maintaining, like any software, which will cost more money. The idea of using computers to help us fill in the gaps in serious mathematical literature is currently to a large extent a naive dream.

My idea of how to proceed is by educating undergraduates, so that they can see that computer proof verification exists, and they can see that at undergraduate level it is nowadays fairly straightforward, and fun. I believe that the current generation have left pure mathematics in somewhat of a mess, and I want to train the next generation in the tools which I believe will somehow, one day, start helping to tidy it up. I want them to drain the swamp that we have created. The time frame on this: it will still not be solved when I die. But that is merely an indication of how bad the mess is. Much of pure mathematics (e.g. current work on the p-adic Langlands program) is extremely beautiful, but at the end of the day much of it is not useful beyond our discipline and may never be useful beyond our discipline. If it is not right either — why are we wasting our time doing it? Is “mostly right” really good enough for us?

Advertisement