Lots of proofs are irreducibly ugly, even when the idea behind them is simple. Just too many edge cases and details. Automatic proof systems can avoid this.
I think of it much like garbage collection and higher order functions. The machine code of a garbage collected program might be messier than a manually managed one. But python code is prettier than c code.
but think about the following two situations: (1) you have serious doubt as to whether a statement is true. presenting a proof removes all doubt. Computer proofs, no matter how ugly, are a win for this situation (2) you have overwhelming experimental evidence that something is true and you want a mathematical proof to help you understand why it is true. Computerized proofs are less helpful here - this is where you want an elegant and simple proof. it should be very intuitive how the result depends on the assumptions. it should be something you'll be able to remember when you're 70 years old.
My guess is that we will instead have proof assistants. Basically, what will happen is that a human will come up with the big idea which motivates the proof, and will direct the proof assistant through the details.
I'm thinking something along the lines of Isabelle or Coq + ProofGeneral, except of course much better.
A person assisted by a computer can play better chess than any human, and also better than any computer.
Maybe it will be the same here.
In fact it happens in much the same fashion as you described. It's like writing a python port of a C program. You can abstract out the details until you have essentially reduced the proof to a chain of concepts.