Category Archives: General


The problem This post is about the equation . This special case of the binomial theorem is the sort of thing that we would expect incoming students at my university to know, or at least to be able to compute … Continue reading

Posted in General, Learning Lean, tactics | Leave a comment

Function composition

Here’s some musing about functions, finishing with a cool trick which Sebastian Ullrich showed me. If you don’t know what ((∘) ∘ (∘)) means, read on! Lambdas The “functional programming” way of thinking about functions is not usually taught to … Continue reading

Posted in General | Tagged | Leave a comment

Proofs by induction

Term is over and I have spent the entire day thinking about induction. I was mainly concerned about the fact that induction somehow seemed hard for mathematicians to do in Lean. Even proving that the sum of the first n … Continue reading

Posted in General | 3 Comments


Kenny Lau and I just defined a scheme in Lean! The reason I am excited about this is that although most computer proof verification systems have plenty of definitions in, e.g. most of them seem to have stuff like groups … Continue reading

Posted in General | Leave a comment

Which definitions do we want in our library?

I re-read Theorem Proving In Lean over the weekend. The first time I read it was over the summer, when I was learning the basics of Lean, and I got a lot out of it. This time I knew something … Continue reading

Posted in General | Leave a comment

What Xena is not.

A lot of people have asked me questions about Xena and it makes me realise that I’ve not explained some of it clearly enough. At this point, Xena is an almost-empty library of undergraduate level mathematics, written in a programming … Continue reading

Posted in General | Leave a comment

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 … Continue reading

Posted in General | Leave a comment