Category Archives: Type theory

Thoughts on the Pythagorean theorem

Pythagoras’ theorem says that a square is equal to two squares. What does equality mean here? Continue reading

Posted in General, Olympiad stuff, Type theory, undergrad maths | Tagged , , | 8 Comments

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

Equality, specifications, and implementations

There are lots of kinds of equalities in Lean. Here’s some basic things that a mathematician needs to know to understand what’s going on Continue reading

Posted in Algebraic Geometry, General, Type theory | Tagged , , | 6 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 invisible map

Is a subgroup of a group a group? Is 3 a topology on 2? Is a natural number a real number? Decisions like this have consequences. Continue reading

Posted in Type theory, undergrad maths | Tagged , , , | 7 Comments