Category Archives: computability

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

Proofs are not programs

A proof, in the sense understood by modern mathematicians, is not always a program. Continue reading

Posted in computability | Tagged , , , | 4 Comments