Proofs are almost never "irreducibly ugly." What has generally happened in the past is that mathematicians have abstracted the "ugly" parts of a proof, so that

Proofs are almost never "irreducibly ugly." What has generally happened in the past is that mathematicians have abstracted the "ugly" parts of a proof, so that one only has to refer to a mathematical object (object in the OO sense). Ugly proofs for basic theory are usually the primary motivation for mathematicians to invent new mathematical abstractions. In fact, when some mathematician is said to have "reinvented a field of mathematics," it usually means that he has found a particular abstraction or perspective that allows for a simplification of the given field. 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.