# Category Archives: General

## (a+b)^3

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

## 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

## 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

## Schemes!

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

## 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

## 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

## 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