Author Archives: xenaproject

About xenaproject

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.

Beyond the Liquid Tensor Experiment

The liquid tensor experiment is now fully completed. Continue reading

Posted in Algebraic Geometry, liquid tensor experiment | Tagged , | 4 Comments

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

Advertisement

Posted in Machine Learning | Tagged , , , , | Leave a comment

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

Posted in Uncategorized | Tagged | 2 Comments

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

Posted in Uncategorized | Leave a comment

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

Posted in Uncategorized | Tagged | 3 Comments

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

Posted in Uncategorized | Leave a comment

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

Posted in Uncategorized | Tagged , , | 22 Comments

The trace of an endomorphism (without picking a basis)

Did you pick a basis when doing a linear algebra question about finite-dimensional vector spaces? Did you need to? Depends on what you mean. Continue reading

Posted in computability, undergrad maths | Tagged , | 16 Comments

Induction on equality

In type theory, equality has a definition, and basic facts about it such as symmetry and transitivity can be proved from more fundamental principles. Continue reading

Posted in M1F, M40001, Type theory, undergrad maths | Tagged , | 8 Comments

Induction, and inductive types.

Induction in Lean isn’t just something which you do on natural numbers. Continue reading

Posted in Learning Lean, Type theory | Tagged , | 9 Comments