Category Archives: General

What is the Xena Project?

Note (added June 2019); this (below) is an old blog post from 2018. You should really read the updated one here but I’ve left this original one just to preserve history. The current aims and ambitions of the Xena Project … Continue reading

Posted in General, Imperial, undergrad maths | 8 Comments

Formalising mathematics — a mathematician’s personal viewpoint.

Here is an overview of my current thoughts on formal proof verification systems in modern mathematics. 3d computer modelling software such as Blender can make virtual versions of abstract 3d mathematical figures such as truncated dodecahedra and so on. This … Continue reading

Posted in General, Uncategorized | Tagged | 2 Comments

Summer project

I am running a summer project with some students. I’ve sort-of lost count of how many; I think that around 25 people expressed an interest, but some didn’t start yet. In practice we seem to get around 10-15 people coming … Continue reading

Posted in General | Leave a comment


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