The goal of the Xena Project is to get mathematicians, especially undergraduates, using computer proof verification software. This software can be used to check proofs of undergraduate level theorems, solve problem sheet questions and so on. The software turns maths questions into levels of a computer game. The main software we use is called Lean, and we mathematicians cannot get anywhere without also using mathlib, Lean's maths library. Note: instructions for installing Lean and mathlib are here.
Mathlib is an open source project worked on by volunteers. One of our goals, currently coming along nicely, is to get the main results of all of the pure maths courses in Imperial's undergraduate curriculum formalised in Lean's maths library.
The Xena project has weekly meetings on Thursday evenings during Imperial term time in the MLC (the big room on the 4th floor of the Huxley building, the one full of computers). We typically talk about undergraduate or harder level maths, and type some of it up into Lean. We're building a library of undergraduate level pure maths, as well as many other things. Many people are involved, not just Imperial undergraduates. Many of the first year pure courses are done or mostly done, second year algebra is mostly done (but not analysis) and we are making inroads into the more algebraic 3rd year courses. Once we're done, the idea (broadly speaking) is to show the resulting database to an AI and see if it can become a maths expert.
2) Sign up to the mailing list (for Imperial people) for local information about what's happening on Thursday nights.
3) My blog is supposed to be mostly comprehensible to undergraduates.
4) Install Lean and its maths library onto your computer. Or try it online.
5) Dare you try doing an M40001 problem sheet question in Lean?
1) Schemes in Lean, 2019 MEng project by Ramon Fernandez Mir. pdf and formalisation. Ramon formalises Grothendieck's definition of a scheme in Lean.
2) Group cohomology in Lean. 2019 BEng project by Anca Ciobanu. pdf and formalisation. Anca defines H^0 and H^1 and proves the seven term exact sequence.
3) Euclidean geometry in Lean. 2018 summer project by Ali Sever. Formalisation. Ali formalises Tarski's axioms for synthetic geometry in Lean.
4) Many other student contributions from the summer of 2018.
The projects below are not projects I supervised, but are more examples of young mathematicians using Lean to do mathematics.
5) Combinatorics in Lean. Project by Bhavik Mehta written for PCC2020. docs and formalisation. Bhavik is a PhD student in the mathematics department in Cambridge and he formalised the first part of Imre Leader's Cambridge Part III combinatorics course.
6) Compact closed unit ball implies finite-dimensional. Project by Lambert A'Campo and Ashvni Narayanan. Formalisation. Lambert and Ashvni formalised a theorem about unit balls in normed vector spaces for a computing project they did for the London School of Geometry and Number Theory.