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
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 Type theory, naturals, integers
8 Comments
Proofs are not programs
A proof, in the sense understood by modern mathematicians, is not always a program. Continue reading
Xena 