Advertisements
Author Archives: xenaproject
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
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
