Author Archives: xenaproject

About xenaproject

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

(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

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

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

Posted in Uncategorized | 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

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

Posted in Learning Lean | 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

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

Posted in Uncategorized | Leave a comment

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

Posted in Learning Lean | Leave a comment