# Author Archives: xenaproject

## Working with integers

The integers. Lean has integers inbuilt as part of the core library. You can call them int if you want to be old skool, but if you type \Z (and then hit the space bar) in VS Code or emacs … 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! And M1F theorems.

Lean now has complex numbers! Now all we need is sine and cosine and we might be able to prove de Moivre’s theorem! The reason I’m interested in this is that I thought that it would be interesting project to … Continue reading

## How to install mathlib and keep it up to date

Overview I’m going to explain how to install the current (bleeding edge) version of lean and mathlib, and set up a project directory on your (unix or windows or mac) computer where you can write lean files which use the … Continue reading

## Which definitions do we want in our library?

I re-read Theorem Proving In Lean over the weekend. The first time I read it was over the summer, when I was learning the basics of Lean, and I got a lot out of it. This time I knew something … 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