Advertisements
Category Archives: Uncategorized
2+2=4
I am interested in teaching and outreach, and often get asked to give talks to schoolkids. I gave one today, to a room full of year 10 kids (aged 14-15), and I showed them Lean. This was the youngest group … Continue reading
Posted in Uncategorized
Leave a comment
A word on BIDMAS
Maybe it’s not called that in other countries, but in the UK BIDMAS (which I swear was “BODMAS” when I was at school, or maybe I just went to a weird school) was the rule that was used to figure … Continue reading
Posted in Learning Lean, Uncategorized
Leave a comment
Formalising mathematics — a mathematician’s personal viewpoint.
Here is an overview of my current thoughts on formal proof verification systems in modern mathematics. 3d computer modelling software such as Blender can make virtual versions of abstract 3d mathematical figures such as truncated dodecahedra and so on. This … 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
Posted in Uncategorized
Leave a comment
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
Recent student successes
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
Posted in Uncategorized
Leave a comment
What maths is already in Lean?
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
Posted in Uncategorized
1 Comment
