I've just started working through Type Theory and Formal Proof, and in this blog I'll be working through the exercises.
I previously worked through beginner courses on maths proofs, Lean for formalising simple maths proofs, Lisp and Haskell.
My overall aim is to understand how type theory can be used to check mathematical proofs.
