Computers aren't some magical machines that instantly understand what we mean.
At some point somebody has to write the code to implement those 'rules'. Which then opens up exactly the same problems (if not more) than if you just verified by hand.
Well, yes, we would have to convince ourselves of the validity of the code that checks the proofs. But the thing is once we made one proof checker whose code we were really confident about, the checking would be over because we could use it for any proof. Whereas with human verification of proofs each new proof is a new checking job.
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).
At some point somebody has to write the code to implement those 'rules'. Which then opens up exactly the same problems (if not more) than if you just verified by hand.