Maths Having fun with theorem proving, proof checking, combinators, categories, λ, and the Curry-Howard correspondence in general.