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?
There have been (and continue to be) many approaches to this, in fact the term Good old fashioned AI basically refers to this. It is very interesting that significant progress has not been made with this approach. This has led to greater use of statistical techniques, such as support vector machines or Bayesian networks. A basic difficulty with any approach to AI is that many techniques merely change the problem of learning, generalisation and problem solving into another form rather than solving it. E.g. Formal methods for software development move the problem from that of programming to that of formal specification. It's not clear that creating the specifications is any less error prone than the creation of the original program.
On the other hand there are enormous benefits to turning any knowledge into a form that a computer can manipulate. There has been some progress in doing this for mathematics. It is possibly one of the most depressing consequences of Godel's theorem that there has not been more work in this area. Writing proofs informally on paper doesn't get around Godel's theorem, it just makes the work harder to validate.
It's also a good challenge for those who feel that AI is just a matter of correctly applying Bayes theorem, as it is not clear how it could be applied to solve this problem.