A lot of people have asked me questions about Xena and it makes me realise that I’ve not explained some of it clearly enough.
At this point, Xena is an almost-empty library of undergraduate level mathematics, written in a programming language called Lean.
By the end of term, Xena will “know” M1F in the following very weak sense: I will (hopefully) have typed up all of the lectures and all of the example sheet questions and solutions into her language. In return, she will have checked all the proofs and solutions for me. Here we are playing to Xena’s strengths. She is careful and pedantic, and she can remember stuff we’ve told her.
Xena is not going to be doing your homework any time soon. Although she is a careful checker, she is incapable of having her own ideas at this point.
On the other hand, Xena is quite capable of going through a list of theorems that she knows and attempting to use them to solve problems. Indeed she can look through such lists very quickly and efficiently and put them together in all manner of ways. That’s one advantage of digitising them! The fact that most of the ways she puts them together will be really stupid might be compensated for by the fact that she will be being stupid at a tremendously quick rate.
I have absolutely no idea how good she will be at being able to solve problems in practice though, and I suspect that, initially at least, she will be rather poor at it. This is one thing I will learn more about as the term goes on. The reason I don’t know is that I suspect that nobody really knows. There are a few data points, produced by teams of researchers. Let’s get another data point, and instead of using a small team of expert researchers let’s use a large team of people who are interested in learning how mathematics works because they want to pass a degree in it.
One personal goal I have for the term is to teach Xena M1F in this very weak sense explained above — I want her to check all the theorems in the course and to check all the problems on the problem sheets. But one consequence of this is that anyone else who learns her language will be able to attempt to solve the M1F problem sheets in this language, and they will know at the end of it if their solution is correct or not, because if it compiles then it’s correct and if it doesn’t then it’s incomplete or wrong.
If I can teach this language well enough that other people can start typing up other problem sheets from other courses in this language — then maybe people who are not doing M1F can start to benefit from Xena’s very careful approach to mathematics.
So when do all the fireworks start with machine learning and AI and trying to create some gigantic mathsbot which will prove the Riemann Hypothesis? All of this is currently just a completely out-of-reach dream, and if proof strategies do not scale well then it might well remain a dream.
On the other hand, I firmly believe that if a student were to first learn the language, and then attempt to engage with some course material — from any pure mathematics undergraduate course — then trying to talk to Xena about this material may well teach them something about the nature of the material that they may not have known before. It might, for example, make them think more deeply about what is going on in the material. It might help them understand it better. It might teach them subtleties that they had not appreciated. It will not do their homework for them, but it might help them learn the material. And at the end of the day, as an educator, I am very interested in facilitating learning. That is an important part of my job, and that is one of the reasons that I started this project.