Xena is a virtual undergraduate, studying mathematics at Imperial College London. Xena is a project set up by Kevin Buzzard, the author of this blog. I teach a course at Imperial called M1F, an introduction to proof course. This term I am teaching this course both to the real undergraduates and to Xena.
Over the next few years I hope to train some of the real undergraduates at Imperial to speak in Xena’s language, which is called Lean. Firstly I will be distributing the problem sheets for this course both in traditional pdf format and also in Lean format. This means that any Imperial undergraduate who is taking M1F (or who has taken it in the past) will have the opportunity to tackle the problem sheets in this language. And secondly, I will be offering these undergraduates the opportunity to teach Xena any other mathematics which undergraduate mathematicians are taught here at Imperial.
Will we be able to get her through the end of year exams though?
I think at this point, a more realistic goal is: will we able to get her to comprehend the solutions to last year’s exam, by the time everyone else is revising?
For more information on Xena, click on About Xena above.