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.

What is homotopy type theory? An amateur speaks.

Learning some Euclidean geometry helped me to understand the basics of what homotopy type theory is. Continue reading

Posted in undergrad maths | Tagged , , , , , , | 10 Comments

Proofs are not programs

A proof, in the sense understood by modern mathematicians, is not always a program. Continue reading

Posted in computability | Tagged , , , | Leave a comment

The inverse of a bijection.

Constructing the inverse of a bijection in Lean can be tricky for beginners. Continue reading

Posted in Learning Lean, M1F | Tagged , | 6 Comments

Equality part 3: canonical isomorphism.

I hadn’t planned on writing a third equality post, but my talk at Big Proof 2019 (see slides here) ended up having a huge section about “mathematician’s equality”, and I realised I had more to say about it. Here are … Continue reading

Posted in Uncategorized | Tagged , | 11 Comments

Equality part 2: syntactic equality

Syntactic equality is yet another kind of equality. I am beginning to learn why it matters. Continue reading

Posted in Learning Lean, tactics | Tagged , | Leave a comment

Equality part 1: definitional equality.

I keep meaning to write something about equality in Lean, and on the tube home today I just managed to understand it a little bit better, so perhaps now is the time (although I won’t get to today’s revelation until … Continue reading

Posted in Learning Lean | Tagged , | 1 Comment

Perfectoid spaces!

Patrick Massot, Johan Commelin and I finished our definition of a perfectoid space in Lean! Patrick and Johan are professional mathematicians like me, not Imperial undergraduates, but I am sufficiently excited about the project that I couldn’t stop myself blogging … Continue reading

Posted in Uncategorized | Tagged , , , , , | 4 Comments