An interesting idea! I've long wanted to go through more of his books, and I've also long wanted to learn Coq, so that sounds like an interesting combination.
I learnt it mostly for the sake of learning something new, I didn't really think at the time whether it would be worthwhile. It's a very specific tool developed by people in very specific fields of CS (type theory, compiler verification, but I could be wrong about this), so I just never felt bad about not having a use for it myself.
Encoding (a subset of) the puzzles as SAT problems for something like z3 would be an alternative to Coq.
Have you found it worthwhile to learn Coq?