Author Archives: xenaproject

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.

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

Posted in Learning Lean | 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

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

Posted in M1F | Leave a comment

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

Posted in Technical assistance | Leave a comment

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

Posted in General | Leave a comment

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

Posted in Uncategorized | 2 Comments