Following the theme, a neat repo of Coq proofs I just discovered: https://github.com/stepchowfun/proofs I don't know much about this space, but a gateway drug like this might help me get into it.