# Author Archives: xenaproject

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

## Tonbridge

Going down to Tonbridge to speak to the UK IMO squad. I will give one talk about why 144 is the largest square in the Fibonacci sequence, and then one talk about why 144 is the largest square in the … 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

## Group Theory revision

To all Imperial students — welcome back and good luck in your exams. I was looking at the axioms for a group in Lean today. If you fire up Lean and type #print group (e.g. by clicking here and then … 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

## No confusion over no_confusion

I’ve always been a bit confused about no_confusion. Functions with names like this are occasionally applied in Theorem Proving In Lean but with little explanation (for example in section 10.1 of TPIL they use it twice to prove 2 ≠ … Continue reading

## Mini-tutorial : Currying.

A couple of mathematics undergraduates have asked me about this recently. Currying is something which is important in computer science, but is based on a fact which is trivial mathematically. As it’s not hard to see, → is not associative. … Continue reading