Lean Library currently studying for a degree at Imperial College
This is a library of files written in a computer language called Lean. Lean is an automated proof checker. You can find more information about Lean at
Basically, Lean can understand mathematics, and can check that it doesn't have any mistakes in.
The library is called Xena, and Xena is currently studying mathematics at Imperial College London. To find out more about her, you could check our her blog at
https://xenaproject.wordpress.com/
Xena is a project run by Kevin Buzzard, who teaches the course "M1F : Foundations of Analysis", one of the first courses which a mathematics undergraduate takes at Imperial College. This M1F course contains an introduction to the notion of a mathematical proof, and also definitions of basic concepts in pure mathematics such as sets, functions and equivalence relations. The course was designed by Martin Liebeck and it is based on his book "A Concise Introduction to Pure Mathematics", published by Chapman & Hall.
Students sometimes like typed up course notes for a course, for various reasons. One of the goals of this project is to type up notes for this course but in the Lean language. Once this is done, one could argue that, in some sense, Xena will understand that course.
Another goal is to type up solutions to all of the example sheet questions for this course. Once this is done, we could argue that, in some sense, Xena has done all the example sheets for the course.
A really cool goal would be to get Xena to pass the M1F final exam! In some sense, at least. Could she pass any other exams? How much will be actually be able to teach Xena? Can we get her a degree?
Type up the statement of the first part of the first question of the first M1F example sheet. [note: I typed up last year's Q1 instead]
Type up the proof of the first part of the first question of the first M1F example sheet. [note: I really should type up a new sheet for this year.]
Write an example sheet for this year, so that the previous goals become well-defined.
Type up all of Q1, questions and solutions.