I'm not sure what exactly you're asking. Would you like to read an in-depth survey of the present state of the art in automated theorem proving and automatic verification? Or are you interested in the fundamental question of why these problems are intractable in the great majority of really interesting cases? The former would require expert input, but the latter mostly boils down to some basic observations from the theory of computation, the foundations of math, and complexity theory.
Any such information would be appreciated, though in this post I'm primarily asking "what would be the benefits of having sophisticated tools for automatic proving and verification?"
Automated theorem proving *sounds like* a natural extension of many useful trends and a solution to many current problems. To me, it seems obvious that there will be a need for the formalization of the mathematics (up to and beyond the boundary of mathematics with real-world applications) as well as the routine checking of software for 100% intended performance. Secure networks and software in particular could be an important safeguard against AI.
Yet I haven't heard much of it; the implementation difficulties must be considerable given that there are substantial and predictable benefits to the widespread use of automated theorem proving. Anyone with experience in the field?