# Category Archives: M40001

## Induction on equality

In type theory, equality has a definition, and basic facts about it such as symmetry and transitivity can be proved from more fundamental principles. 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

## 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 division, division by zero
12 Comments

## The natural number game — an update

I just pushed an update to the natural number game. I’m rather pleased with how this has all worked out. I started off thinking it was kind of a game, but the explanations turned out so wordy and now I … Continue reading