Category Archives: Learning Lean
Induction, and inductive types.
Induction in Lean isn’t just something which you do on natural numbers. Continue reading
Formalising Mathematics : workshop 4 — topology
OK, an overview of this week: we’re doing topology. I was going to introduce filters but I decided to put them off for one more week, so this week it’s topology the way it is traditionally taught in mathematics departments. … 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
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
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
The Sphere Eversion Project
Patrick Massot has written a blueprint for sphere eversion. This marks the beginning of a community formalisation project. Continue reading
The complex number game
The complex number game, and the Xena Project’s first steps into Twitch and Discord. Continue reading
Xena Project Thursday meetings start with talk tomorrow 21st May
The Complex Number Game — proving basic stuff about the complexes in Lean Continue reading
Xena 