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.

Posted on June 19, 2019

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

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

Proofs are not programs

Posted on June 15, 2019

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.

Posted on June 11, 2019

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.

Posted on June 2, 2019

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

Posted on May 25, 2019

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.

Posted on May 21, 2019

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!

Posted on May 11, 2019

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