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.

Lean Together 2021

A discussion of some of the talks from the Lean Together conference. Continue reading

Posted in Uncategorized | Tagged | 6 Comments

The end of the summer.

It’s the end of the summer now, so it must finally be time to talk about the summer projects, and the things which happened since then. Continue reading

Posted in Imperial, Learning Lean, M40001, undergrad maths | Tagged | Leave a comment

Liquid tensor experiment

Peter Scholze suggests a mathematical formalization challenge. Continue reading

Posted in number theory | Tagged , | 11 Comments

Thoughts on the Pythagorean theorem

Pythagoras’ theorem says that a square is equal to two squares. What does equality mean here? Continue reading

Posted in General, Olympiad stuff, Type theory, undergrad maths | Tagged , , | 8 Comments

Two types of universe for two types of mathematician

Thank you Johan for pointing out to me that the mathlib stats page had got really good! But one thing that made me laugh is that somehow on their stats for commits I see I have done just enough to … Continue reading

Posted in Uncategorized | Tagged , , | 7 Comments

Lean for the Curious Mathematician 2020

Lean for the Curious Mathematician 2020 just happened. It was interesting. Continue reading

Posted in Learning Lean | Tagged , | Leave a comment

Division by zero in type theory: a FAQ

How can a theorem prover use the convention that 1/0=0 and still be consistent? Continue reading

Posted in Learning Lean, M1F, M40001, Type theory, undergrad maths | Tagged , | 12 Comments

Equality, specifications, and implementations

There are lots of kinds of equalities in Lean. Here’s some basic things that a mathematician needs to know to understand what’s going on Continue reading

Posted in Algebraic Geometry, General, Type theory | Tagged , , | 6 Comments

Teaching dependent type theory to 4 year olds via mathematics

What is the number before 0? Who cares! How do children model numbers? An experiment with type theory. Continue reading

Posted in computability, Learning Lean, number theory, Type theory | Tagged , , | 8 Comments

Mathematics in type theory.

An explanation of how to set up mathematics using universes, types, and terms Continue reading

Posted in Learning Lean, Type theory, undergrad maths | Tagged , , , | 24 Comments