1) Many of us are interested in the verification of computer systems.
Thus, the types of mathematical proofs we primarily wish to verify are
rather applied and mundane ones.
2) There are areas of pure mathematics, notably in combinatorics, where one
encounters complexities quite similar to those which make proofs of
computer system correctness so difficult and tedious.
3) If one cannot build theorem provers that prove useful to computer
engineers, it seems quite likely that one cannot solve the harder
problem of theorem provers for pure mathematicians.
4) I also find it very doubtful that mathematics suffers from a problem
of incorrect theorems that will only be rooted out by QED.
Leslie Lamport, who seems to be the main publicist of the contrary view,
has, in my ever so humble opinion, failed to understand the difference
between computer programs that will not compile with a simple error and
proofs that serve the purpose of communication even if they contain
errors.