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.

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

Sessions moved to Mondays in weeks 7 and 8

I can’t make Thursday 16th or Thursday 23th November, so the Imperial sessions for those weeks will take place on Monday 13th and Monday 20th November. Sorry for the inconvenience. Kevin

Posted in Imperial | Leave a comment

Building the non-negative integers from scratch

It’s not actually that hard to build the non-negative integers from scratch in Lean. Let’s call them xnat, because Lean already has an inbuilt nat. The code just looks like this: inductive xnat | zero : xnat | succ : … Continue reading

Posted in Learning Lean | 2 Comments

Rational powers

Lean’s core library has no support for rational or real numbers 😦 They are however in the maths library — or we can just make some fake real numbers and use them instead. — let’s define the real numbers to … Continue reading

Posted in Learning Lean, M1F | Leave a comment

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

Posted in Uncategorized | Leave a comment


Lean uses something called type theory. This can be a little bit counterintuitive to mathematicians. For example there are lots of different kinds of 7. The core Lean library provides us with the natural number 7 = 7:nat, and the … Continue reading

Posted in Learning Lean | Leave a comment