### Categories

# Author Archives: xenaproject

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

## Types

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