# Author Archives: xenaproject

## Proofs are not programs

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

## The inverse of a bijection.

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

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

## Equality part 2: syntactic equality

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

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

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