That's not the issue. The issue has always been that of knowledge and epistemology.

This is why the computer-assisted proof of the four-color theorem was such a talking point in math/cs-circles: how do you "really" know what was proven. This is slightly different from say an advisor who trains his students : you can often sketch out a proof, even though the details require quite a bit of work.

The most difficult part of automated theorem proving is not the "tactic" part, but actually in the formulation.

(Theory building is quite hard in math; the computation side is only hard after a point).