Category Archives: Imperial

The end of the summer.

It’s the end of the summer now, so it must finally be time to talk about the summer projects, and the things which happened since then. Continue reading

Posted in Imperial, Learning Lean, M40001, undergrad maths | Tagged | Leave a comment

The Sphere Eversion Project

Patrick Massot has written a blueprint for sphere eversion. This marks the beginning of a community formalisation project. Continue reading

Posted in Imperial, Learning Lean, Type theory | Tagged , , , , , , , | 2 Comments

Summer projects 2020

Undergraduate mathematician? Not much to do in July and August? Come and work with me! Continue reading

Posted in Imperial, Learning Lean, Uncategorized, undergrad maths | Tagged , | 2 Comments

My algebraic geometry course

The union of two affine algebraic sets is an affine algebraic set. Continue reading

Posted in Algebraic Geometry, Imperial, Learning Lean, M4P33, undergrad maths | Tagged , , | 3 Comments

Prove a theorem. Write a function.

New maths PhD students Lambert A’Campo and Ashvni Narayanan have proved that a normed real vector space with compact unit ball is finite-dimensional in Lean! [update added a few days later: ROFL Sébastien Gouëzel on the Lean chat complained that … Continue reading

Posted in General, Imperial, Learning Lean | Tagged , , , , , , , , | 6 Comments

Lean does not (yet) have real manifolds.

Lean does not yet have real manifolds, but there has been recent progress. Continue reading

Posted in General, Imperial, undergrad maths | Tagged , , , , , , , , , , , , , , , , | 7 Comments

Lean in LaTeX

Patrick Massot wrote a formatter, which can turn Lean code into beautiful LaTeXxy html. The undergraduates and I have been formalising Imperial’s first real analysis course M1P1 in Lean. Put them together and you get a 21st century proof of … Continue reading

Posted in Imperial, undergrad maths | Tagged , | 2 Comments

Maths undergraduate example sheets

I’m teaching a course called M1F this term — the basic “introduction to proof” course which all first year maths (and joint maths/computing) students have to take at Imperial College London. The course is supposed to be managed via our … Continue reading

Posted in Imperial, Learning Lean, M1F, tactics, undergrad maths | Leave a comment

What is the Xena Project?

Note (added June 2019); this (below) is an old blog post from 2018. You should really read the updated one here but I’ve left this original one just to preserve history. The current aims and ambitions of the Xena Project … Continue reading

Posted in General, Imperial, undergrad maths | 9 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