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.

Formalising mathematics — a mathematician’s personal viewpoint.

Here is an overview of my current thoughts on formal proof verification systems in modern mathematics. 3d computer modelling software such as Blender can make virtual versions of abstract 3d mathematical figures such as truncated dodecahedra and so on. This … Continue reading

Posted in General, Uncategorized | Tagged | 2 Comments

Happy birthday Xena!

It was a year ago today that I emailed Inkeri Hibbins, a wonderful administrator at Imperial College London, and asked her if she could email all the Imperial maths and joint maths/computing undergraduates and tell them about my new Thursday … Continue reading

Posted in Imperial, M1F, undergrad maths | 3 Comments

What is a uniform space? How some computer scientists think about completions.

This is post 2 of 2 posts both of which are attempts to explain some basic mathematical definitions which I have never seen covered in an undergraduate mathematics course. These definitions play a rolein Lean because it’s important to set … Continue reading

Posted in undergrad maths | 2 Comments

What is a filter? How some computer scientists think about limits.

This is post 1 of 2 posts both of which are attempts to explain some basic mathematical definitions which I have never seen covered in a mathematics course. This one is on filters, and the next one will be on … Continue reading

Posted in undergrad maths | 3 Comments

617 is prime

More number theory today. Clara List and Sangwoo Jo were trying to do a question from the third year number theory example sheet; to work out whether 605 was a square modulo 617. They decided to assume the law of … Continue reading

Posted in number theory, tactics | Leave a comment

Quadratic Reciprocity and (p^2-1)/8

The law of quadratic reciprocity. The jewel in the crown of mathematics! Still not proved in Lean! Clara List and Sangwoo Jo were thinking about this today. They formalised the statement. There are two “supplements” to the law, describing when … Continue reading

Posted in Learning Lean, number theory | 1 Comment

Summer project

I am running a summer project with some students. I’ve sort-of lost count of how many; I think that around 25 people expressed an interest, but some didn’t start yet. In practice we seem to get around 10-15 people coming … Continue reading

Posted in General | Leave a comment