I love math books with great exercises, I just wish I could code them up in a theorem prover and solve and store my proofs that way. I've tried a bunch of tools but haven't found a language or workflow that really meets the needs for computer assisted study of mathematics.