I don't know if you have tried to encode a reasonable sized theorem/proof in Coq or Agda. It is worth giving it a shot if you haven't. It is kind of eye opening (and both these systems are significantly different from each other).

The real problems I have had with that so far has been a) the extreme precision required in encoding the problem. This exceeds what you normally require in a paper proof b) ensuring that the prover "understands" the necessary background math that you are basing the proof on. i.e. Libraries of math. This situation is improving with time c) The search strategies that the prover is using to verify steps is sub-optimal/does not work for your case. When a human reads/writes/verifies a proof there is a lot of cognitive shortcuts and background information coming in to play. But for a prover this has to be spelled out precisely. Provers tend to come with a set of built-in "tactics" to do this and (often) allow new tactics to be written out. (Coq, for example, allows you to write your own tactics for example. But it is not exactly fun). Again this is slowly improving.

For most mathematicians this process is a high overhead one (as yet).