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.
“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.