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.

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

Formalising Mathematics : workshop 8 — group cohomology

A brief description of group cohomology H^0 and H^1, plus links to how to formalise this stuff in Lean. Continue reading

Posted in Uncategorized | 5 Comments

Formalising Mathematics : workshop 7 — quotients

Is a quotient a set of equivalence classes? I think it’s something a bit more general than that. Continue reading

Posted in formalising mathematics course, M1F, undergrad maths | Tagged , | 7 Comments

Formalising Mathematics : workshop 6 — limits

I talked about limits of sequences of real numbers in workshop 3, but this week I come back to them, because this week we’ll see that the usual ten-line proof that if and then can be replaced by a two-line … Continue reading

Posted in Uncategorized | Leave a comment