Category Archives: M40001

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

Posted in Imperial, Learning Lean, M40001, undergrad maths | Tagged | Leave a comment

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

Posted in Learning Lean, M40001, undergrad maths | Tagged , | 19 Comments