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?
Do you think the current generation has made more of a mess than previous generations (if we adjust for the total number of mathematicians)? I’m curious as to at what point in the past there would be a better ratio of mathematics that it is correct, or that is useful beyond the discipline. Do you think the situation is any better in any other science (or any other field of study)?
I think pure mathematics has just run into a bunch of different problems over the centuries, but has always survived. There were issues with early work in real analysis because people had different ideas about what the real numbers were (in particular whether they contained infinitesimals). I should learn more about what the issues were here. Maybe when the “completion of the rationals” definition caught on, those problems then had to be dealt with, and of course they were. I guess I know more about what happened in alg geom, because of my MO question https://mathoverflow.net/questions/19420/what-mistakes-did-the-italian-algebraic-geometers-actually-make and the great answers it generated. I think the problems now are slightly different. Someone emailed me today and told me about a paper in their area which is published in a prestigious journal and which is wrong, but it’s OK because all the experts know it’s wrong. Experts are also aware of gaps in the literature and how to fill them in, or who to ask. But I am a bit scared that this knowledge will die out. Here’s a question. Loads of people are writing papers which rely on theorems which Jim Arthur has announced but not yet produced complete proofs of. Jim Arthur is of course a super-smart person and I believe that the expert opinion is that the things he has announced are all going to work out fine. But what if Jim Arthur gets hit by a bus tomorrow? Same question for classification of finite simple groups. A dwindling group of people are frantically trying to write everything down. What if it doesn’t get done, and then what if in 20 years’ time we suddenly realise that the expertise is now lost because smart young people are not going into finite group theory and now nobody knows how the proof goes?
I think the answer to your question is that I perceive the state of mathematics today to be a new and interesting kind of mess, different to other messes it has been in.
I should also stress the point I tried to make in my post today, which is that I certainly do not think that formal proof verification systems are going to save us all. I think the problem is far more complex. But what I want to argue is that one should be able to read the literature without having to be “in with the in crowd”, the people who know what is right, what is suspect, and what is outright wrong.
LikeLiked by 1 person
PS I should add that I know absolutely nothing about the way other sciences “actually work in practice” when it comes to who believes what. Pure maths is different here. Every single well-formulated mathematical statement can be in a very small number of very well-defined boxes: “Proved” (in ZFC, say), “Conjectured but not proved”, “Proved to be false” and then of course stuff like “known to be independent” etc. In other sciences there are far more boxes. I am concerned that we are getting some extra junk boxes in pure maths — “Proved modulo unpublished results which were announced by an expert X years ago and for which no proof may ever be forthcoming”, for example. My question is whether pure mathematics is happy to rely on results in those boxes.
Edits (which I can’t make to comments apparently) : prestigious journal -> respectable journal, and it is not OK. See comment below.
Kevin, that’s not quite what I said in the email you refer to. I didn’t say “a prestigious journal”: I said “a respectable journal”. More importantly, I didn’t say it was OK. I don’t think it’s OK and I did what I could to stop it happening, which was to reject the paper when I was asked to referee it and to let the experts know what I thought. What does make it OK in this particular case is that the paper isn’t really important anyway. If you believe the result it claims it is not likely to do you much harm (the result may even be true) and if you do try to use it you will need to look at the proof, which will then shred itself before your eyes like that Banksy. So in the damage is slight, but by luck.
I will edit. Thanks.
How about MetaMath Proof Explorer?
One of the reasons that Lean has so much basic functionality essential for doing any mathematics at all (for example a working theory of finite sets) is that Mario Carneiro, someone with a vast experience of writing MetaMath proofs, is the main driving force behind Lean’s maths library. I guess he knew exactly what was needed to start the whole thing off. One huge advantage of Lean over metamath is that you can write advanced tactics in Lean which will do jobs like solving basic inequalities over the reals, or basic identities in ring theory (and formally verifying that the solutions are correct of course). I think Tom Hales’ analogy https://jiggerwit.wordpress.com/2018/04/14/the-architecture-of-proof-assistants/ is an interesting way of comparing the two proof assistants.
Pingback: Harris versus Buzzard | Persiflage