Category Archives: computability

The trace of an endomorphism (without picking a basis)

Did you pick a basis when doing a linear algebra question about finite-dimensional vector spaces? Did you need to? Depends on what you mean. Continue reading

Posted in computability, undergrad maths | Tagged , | 16 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

Proofs are not programs

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

Posted in computability | Tagged , , , | 5 Comments