I had a lot of fun going through incredible.pm/ which is gamified writing set theory proofs. Following along with Software Foundations[0] also teaches you how t

I had a lot of fun going through incredible.pm/ which is gamified writing set theory proofs. Following along with Software Foundations[0] also teaches you how to use the Coq proof assistant and write proofs in it, which I found entertaining. I think of proof solving as manipulating symbols from A to B, with a proof that each intermediate transformation is valid and sound. 0: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/