Months ago I dipped my toe into Lean+mathlib as a proof assistant. I wanted to know how it worked. That led me to start learning about "propositions as types" and "inhabitants as proofs"...

I've somehow managed to get to the end of Chapter 7 of Type Theory and Formal Proof - almost half way.

I'm working through all the exercises and writing them up - caution, some may be wrong - but it helps me learn better.

https://type-theory-and-formal-proof.blogspot.com/p/contents.html

#maths #typetheory #ProofAssistants