When I worked as an RA while getting my BSCS (and for a time during my first post-college job), I spent quite a bit of time with ACL2 (a language, logic, and pr

When I worked as an RA while getting my BSCS (and for a time during my first post-college job), I spent quite a bit of time with ACL2 (a language, logic, and proof assistant using a first-order variant of common lisp). I spent a lot of time applying ACL2 to my research area (information flow analysis for secure systems), and I feel your pain re: proof strategies. It was almost like learning how to prove things again (e.g. learning new induction strategies that matched the logical framework used by the tool). That said, there was an incredible amount of freedom in knowing that if the tool accepted a proof, it was (probably) correct. Occasionally I would stumble on to a strategy without knowing why exactly it worked, and the interactive nature of the tool helped me gain understanding by letting my apply transformations to terms interactively without having to worry about whether I screwed up some minor detail. I'd love to see one of these tools (though, probably not ACL2 at this point - first-order logic frequently felt limiting (e.g. when proving things about parameterized equivalence relations)) used in a book covering some math topic I'd like to learn, as interactive formalism seems well-suited to self-exploration (you don't need an instructor to point out your trivial errors)