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
Xena 