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.

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

## 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

## Formalising Mathematics : workshop 5 — filters

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

| Tagged , | 5 Comments

## Formalising Mathematics : workshop 4 — topology

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

## Formalising mathematics : workshop 3 — sequences and limits

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

| 1 Comment

## Formalising mathematics : Workshop 2 — groups and subgroups

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

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

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.

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