Some proofs in Coq and Idris, exploring by hand how theorem provers and
dependent langs work.

If I start following a resource, I'll put its name below.