[bombastry]

These books are surprisingly satisfying and fun to work through. The instant feedback from the proof checker makes them feel like a game of logic puzzles.

[amw-zero]

There’s another book, Concrete Semantics, that starts off by saying something along the lines of:

“Be careful - interactive theorem proving is addicting.”

It’s so true. You can end up ‘accidentally’ proving things, and when the proof checker accepts the proof it’s a big endorphin rush.

http://concrete-semantics.org/