# Category Archives: Learning Lean

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

## Summer projects 2020

Undergraduate mathematician? Not much to do in July and August? Come and work with me! Continue reading

## No errors.

Does your Lean file contain errors? Try and cut down. Continue reading