# Category Archives: Uncategorized

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