# 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 integers, naturals, Type theory
8 Comments

## Proofs are not programs

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