# Category Archives: Uncategorized

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

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

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

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

## Complex numbers? Intermediate Value Theorem?

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

## How is Xena doing?

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