Author Archives: xenaproject
Lean in 2024
A huge amount happened in the Lean theorem prover community in 2023; this blog post looks back at some of these events, plus some of what we have to look forward to in 2024. Modern mathematics I personally am a … Continue reading
Formalising modern research mathematics in real time
(This is a guest post by Bhavik Mehta) On March 16, 2023, a paper by Campos, Griffiths, Morris, and Sahasrabudhe appeared on the arXiv, announcing an exponential improvement to the upper bound on Ramsey numbers, an open problem since 1935. … Continue reading
Lean 2022 round-up
A brief survey post containing some of the things which happened in the Lean community in 2022. The Liquid Tensor Experiment In December 2020, Fields Medallist Peter Scholze challenged the formal computer proof community to verify one of his theorems … Continue reading
Beyond the Liquid Tensor Experiment
The liquid tensor experiment is now fully completed. Continue reading
The Future of Interactive Theorem Proving?
This is a guest post, written by Zhangir Azerbayev. Zhangir is an undergraduate at Yale, majoring in computer science and mathematics. He completed this work while visiting Carnegie Mellon’s Hoskinson Center for Formal Mathematics. Introduction The history of interactive theorem … Continue reading
Teaching formalisation to mathematics undergraduates
It’s been a hectic 2022 so far, but August is looking a lot calmer; this is the first of hopefully a few blog posts this month catching up on various things. In this post I want to talk about the … Continue reading
2022 Xena Project undergraduate workshop
I have funding to run an undergraduate workshop! When? 26th to 30th September 2022 (the week before term starts for many people in the UK). What? A week-long in person workshop including a bunch of working on group projects in … Continue reading
New year, new teaching material
Imperial College has gone back to in-person teaching so I have 250 new subjects to experiment on, namely the new 1st year maths undergraduates. I’ve spent a few years now trying to figure out how best to teach maths undergraduates … Continue reading
2021 Xena Summer Projects
So I spent July and August supervising mathematics undergraduates who were doing Lean projects in various areas of mathematics. Conformal maps, Euclid’s SAS theorem, nilpotent groups and the Radon-Nikodym theorem are just some of the topics I’ve been engaging with … Continue reading
Half a year of the Liquid Tensor Experiment: Amazing developments
[This is a guest post by Peter Scholze.] Exactly half a year ago I wrote the Liquid Tensor Experiment blog post, challenging the formalization of a difficult foundational theorem from my Analytic Geometry lecture notes on joint work with Dustin … Continue reading
Xena 