Category Archives: Imperial

My algebraic geometry course

Posted on January 14, 2020 by xenaproject

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 affine algebraic set, Algebraic Geometry, M4P33 | 3 Comments

Prove a theorem. Write a function.

Posted on December 7, 2019 by xenaproject

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 Ashvni Narayanan, canonical, collection, compact unit ball, etale cohomology, Grothendieck topology, london school of geometry and number theory, LSGNT, Peter Scholze | 6 Comments

Lean does not (yet) have real manifolds.

Posted on July 17, 2019 by xenaproject

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

Posted in General, Imperial, undergrad maths | Tagged Agda, Bochner Integral, Coq, HOL-Light, Idris, Isabelle-HOL, Jeremy Avigad, Johan Commelin, lean, manifold, Mizar, Patrick Massot, Perfectoid Spaces, Sebastien Gouezel, theorem provers, UniMath, Zhouhang Zhou | 7 Comments

Lean in LaTeX

Posted on February 11, 2019 by xenaproject

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 LaTeX, M1P1 | 2 Comments

Maths undergraduate example sheets

Posted on October 21, 2018 by xenaproject

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?

Posted on October 7, 2018 by xenaproject

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!

Posted on September 21, 2018 by xenaproject

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

Sessions moved to Mondays in weeks 7 and 8

Posted on November 8, 2017 by xenaproject

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

Note for Imperial undergraduates

Posted on October 5, 2017 by xenaproject

The Xena project now has an internal site on blackboard, Imperial College’s VLE. You (Imperial maths and JMC UGs) should all be registered as being able to view it. Email me if you can’t access it. It (only) contains internal … Continue reading →