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

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

Lean for the Curious Mathematician 2020

Lean for the Curious Mathematician 2020 just happened. It was interesting. Continue reading

Posted in Learning Lean | 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

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

Posted in computability, Learning Lean, number theory, Type theory | Tagged , , | 8 Comments

Mathematics in type theory.

An explanation of how to set up mathematics using universes, types, and terms Continue reading

Posted in Learning Lean, Type theory, undergrad maths | Tagged , , , | 24 Comments

The Sphere Eversion Project

Patrick Massot has written a blueprint for sphere eversion. This marks the beginning of a community formalisation project. Continue reading

Posted in Imperial, Learning Lean, Type theory | Tagged , , , , , , , | 2 Comments

The complex number game

The complex number game, and the Xena Project’s first steps into Twitch and Discord. Continue reading

Posted in General, Learning Lean, undergrad maths | Tagged , | 4 Comments

Xena Project Thursday meetings start with talk tomorrow 21st May

The Complex Number Game — proving basic stuff about the complexes in Lean Continue reading

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

Summer projects 2020

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

Posted in Imperial, Learning Lean, Uncategorized, undergrad maths | Tagged , | 2 Comments

No errors.

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

Posted in Learning Lean, Technical assistance, Uncategorized | Tagged , , , | Leave a comment