# 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