Author Archives: xenaproject
Lean Together 2021
A discussion of some of the talks from the Lean Together conference. Continue reading
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
Liquid tensor experiment
Peter Scholze suggests a mathematical formalization challenge. Continue reading
Thoughts on the Pythagorean theorem
Pythagoras’ theorem says that a square is equal to two squares. What does equality mean here? Continue reading
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
Lean for the Curious Mathematician 2020
Lean for the Curious Mathematician 2020 just happened. It was interesting. Continue reading
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
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
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
Mathematics in type theory.
An explanation of how to set up mathematics using universes, types, and terms Continue reading
