Category Archives: Uncategorized

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 →

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 →

Here’s what some of Imperial’s undergraduates have been doing. Blue-eyed Islanders. Chris Hughes typed up a solution to the blue eyed islanders problem! The question is here (M1F sheet 5) (question 6) (and also on Terry Tao’s blog here), and Chris’ solution … Continue reading →

I sit around chatting to Imperial students on Thursday nights, and some of them will be writing Lean code. I encourage various people to work on various projects but in general I am quite happy to let people work on … Continue reading →

As far as I know, neither the complex numbers nor the intermediate value theorem are in Lean. On the other hand, the real numbers, plus all the facts about them that we need, are there, as long as we install … Continue reading →

What have we managed to tell Xena so far? So far I managed to explain to Xena (i.e. type up in Lean) solutions to all the questions on the first M1F example sheet, and some of the questions on the … Continue reading →