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