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.

Induction, and inductive types.

Posted on April 3, 2021 by xenaproject

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

Posted on March 15, 2021 by xenaproject

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

Posted on March 4, 2021 by xenaproject

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

Posted on February 25, 2021 by xenaproject

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

Formalising Mathematics : workshop 5 — filters

Posted on February 18, 2021 by xenaproject

What is a filter on a set? I am kind of getting the hang of it now. Continue reading →

Posted in formalising mathematics course, Imperial, undergrad maths | Tagged , | 5 Comments

Formalising Mathematics : workshop 4 — topology

Posted on February 10, 2021 by xenaproject

OK, an overview of this week: we’re doing topology. I was going to introduce filters but I decided to put them off for one more week, so this week it’s topology the way it is traditionally taught in mathematics departments. … Continue reading →

Posted in formalising mathematics course, Learning Lean, tactics, undergrad maths | Leave a comment

Formalising mathematics : workshop 3 — sequences and limits

Posted on February 4, 2021 by xenaproject

This week we’re going to do limits of sequences, of the kind you see in a 1st year analysis course. These are great fun to do in Lean. Because of Rob Lewis’ linarith tactic (which does the “and now this … Continue reading →

Posted in formalising mathematics course, M1P1, undergrad maths | 1 Comment

Formalising mathematics : Workshop 2 — groups and subgroups

Posted on January 28, 2021 by xenaproject

This is some notes on the second workshop in my Formalising Mathematics course, running as part of the EPSRC TCC. The Lean github repo is here. Groups and subgroups I start with an apology — there was far too much … Continue reading →

Posted in formalising mathematics course, undergrad maths | Leave a comment

Formalising mathematics : workshop 1 — logic, sets, functions, relations

Posted on January 24, 2021 by xenaproject

An introduction to the material in workshop 1 of my “Formalising mathematics” course. Continue reading →

Posted in formalising mathematics course | 2 Comments

Formalising mathematics: an introduction.

Posted on January 21, 2021 by xenaproject

An introduction to the TCC course “Formalising Mathematics” Continue reading →

Posted in formalising mathematics course, Uncategorized | 19 Comments