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 second sheet. I skipped some of sheet 1 Q5 and all of sheet 1 Q6 because Lean’s type theory as it stood couldn’t make sense of these questions. Kenny Lau implemented enough classical set theory in Lean to do the parts I’d skipped. So sheet 1 really is done. You can see the current state of the write-up here.

As for the second M1F example sheet, to do question 1 I needed the floor function and this was not implemented in Lean, but I now know what I’m doing (to a certain extent) so I could implement this function myself. I’ve solved sheet 2 questions 1 and 2, and also 3(a). To solve 3(b) I need to know that the square root of 3 exists, and unfortunately Lean does not have a square root function, so I am having to implement this myself. This is quite interesting stuff — I will prove later on in M1F that square roots exist using sups and infs and completeness of the reals, and this explicit proof translates rather neatly into Lean. So hopefully soon I will be able to convince Lean that the square root of r exists for r any positive real number. Once I’ve done this I think the rest of sheet 2 should be relatively straightforward. The current state of the solutions is here.

Kenny Lau has implemented enough of the theory of sigma fields in Lean to prove some of the basic statements that Prof McCoy has covered in M1S! His Lean write-up is here.

Looking ahead, the definition and basic properties of the complex numbers shouldn’t be too much trouble, although the stuff about sin(theta)+i.cos(theta) might be. The example sheet questions seem to rely on knowing stuff like what the sin of 45 degrees is, which will be tricky as these things will need to be evaluated algebraically rather than geometrically. Then after that we get a little more abstract and actually things will get a lot easier.

I was hoping I’d be able to do the example sheets as quickly as I was releasing them to the students, but I’m getting behind! Need to work harder…

Advertisements

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.
This entry was posted in Uncategorized. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s