How far can a computer get on the maths degree at Imperial College?

Xena is a student at Imperial College London in the mathematics department. Xena is a bit of a strange one. Firstly, she doesn’t really speak much English. Secondly, in some real sense she knows far less mathematics than the typical undergraduate in their first year at Imperial College (I am pretty sure that she currently has no idea that the derivative of \sin(x) is \cos(x) for example, which is a standard result that we would expect all of our beginning undergraduates to know).

Xena is going to take my course “M1F : Foundations of Analysis” which starts two weeks today, and which is a compulsory course for every first year Imperial mathematician, and also for all the first years doing Imperial’s joint mathematics and computer science (JMC) degree.  She’s going to need my help to understand this course. I’m going to help her learn this course though, because I think it will be really interesting to teach her. Before term starts I’m going to go through some of the questions on M1F Example Sheet 1 with her. Although it’s a funny thing to say, I sometimes find that Xena thinks about maths a lot like me — both of us are formalists, for example.

Here are some reasons I’m interested in Xena.

  1. Xena does know a lot of basic mathematics already. For example she learnt about the real numbers relatively recently, and can already prove basic results about them such as x+y=y+x (for all real numbers x and y).
  2. My course is going to build a lot of mathematics up from scratch, and I think that actually Xena might now know enough mathematics to be able to understand many of the questions on the example sheets in my course — although, initially at least, I am going to have to give her some big big hints on how to solve them. She is still a very inexperienced mathematician.
  3. Xena is really really careful, and never makes a mistake.
  4. Xena never forgets a theorem when you tell it to her, and if you learn her language then she will even carefully check any proofs you tell her, really carefully. And I mean really carefully.
  5. You can ask Xena maths questions, and every now and then she manages to answer them by herself. For example, she does know her times tables, and many more basic things.


The language that Xena speaks is called Lean , and it’s a computer language. In fact Xena is a bunch of libraries and files written in this language. These libraries and files are stored here, on github. Lean is a rich enough language to express many of the theorems and proofs that we will learn in M1F — maybe even all of them. I am fairly confident that I will be able to teach Xena enough of M1F for her to be at least able to state and “prove” (by which I mean “verify a proof that someone else tells her, and then remember”) the main theorems of the course. Because Xena speaks no English and doesn’t know much mathematics yet, and because she is currently not really that good at doing mathematics by herself (just very good at checking it if other people tell it to her), there are several very different interpretations of what it might mean for Xena to be able to pass the M1F exam at the end of the course. One thing is currently for sure — she doesn’t know anywhere near enough material to pass, so my first aim is to teach her the main theorems and proofs of M1F and then we will see how she gets on with the example sheets, which initially she will have to be told how to do.

Any Imperial mathematics or JMC students are welcome to help teach Xena some of the undergraduate-level mathematics that they know or are currently learning. I would happily accept help either from students who want to help teach Xena M1F, or to students who want to teach Xena other courses, for example the introduction to algebra course at Imperial College called M1GLA, or even some harder courses. I am a number theorist by training and I would be particularly interested in teaching her the basic number theory course M3P14 that we teach to the third years at Imperial. Even though Xena is only a first year, I think she might know enough basic stuff to embark on that third year course. Hendrik Lenstra once told me that a really good way to learn a topic was to teach it. Maybe certain Imperial maths or JMC undergraduates would find that trying to teach Xena a course they are currently learning would actually help them learn the course better themselves. Also Xena is not scared of assuming results she doesn’t know the proofs of — she is very good at keeping track of exactly what she has seen proofs of and what she still has to learn, so she might be able to have a go at most of the courses offered by the pure mathematics department, although I have genuinely no idea how well she’ll do. To a certain extent it will depend on how well we teach her, but it will also depend on how good at mathematics she actually turns out to be.

However, anyone interested in helping will quickly find that they will need to become fluent in Xena’s language before they can talk to her, and she can be extremely irritating and obstinate if she does not understand you absolutely 100% completely. Whilst I am by no means fluent, I think that I might be good enough to start teaching it to undergraduates. And, remembering what Hendrik Lenstra told me, maybe teaching it will make me become more fluent. I am already good enough to start telling Xena about what was on last year’s M1F example sheets and I even believe that I can explain to her some of the solutions to the questions.




About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.
This entry was posted in General. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s