I sit around chatting to Imperial students on Thursday nights, and some of them will be writing Lean code. I encourage various people to work on various projects but in general I am quite happy to let people work on whatever they like. In the recent past I have encouraged people to prove that matrix multiplication is associative and distributive over matrix addition, that every prime which is 1 mod 4 is the sum of two squares, or that the spectrum of a commutative ring is a topological space. But in the past I have also encouraged people, foolishly, to do stuff which is already in core Lean or mathlib, and this was mainly because I had no good understanding of exactly what was there.

I decided to change this recently, by reading through all of core Lean and mathlib, and making notes on what was there. I now have a far clearer idea myself about what is there, and occasionally find myself telling students that something they are working on has already been done (of course this is no reason to stop working on it, but one might argue that there is still plenty of low-hanging fruit to work on).

So I decided to try and get some of my notes down on this blog, so that students can look for themselves. The current state of what I have managed to write is here, and I hope to update this page over the next few weeks until it contains a reasonable summary of most of the mathematics which Lean already knows. Once I have finished, it might be interesting to then continue by writing a list of all the mathematics which I think Lean could and should know, and which is accessible to undergraduates…

### Like this:

Like Loading...

*Related*

## About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.

It would great if there is a link from Lean or Mathlib to your summary. Many other Lean users would benefit from it, but they may not know of this blog.

LikeLike