Well, it was agony to come up with the original Jordan curve theorem...
Informal proofs make a lot of gestures at expert knowledge to avoid spelling out the mechanics of the less interesting steps in a proof. Sometimes this can be collapsed in a similar way in a formal proof, though through "tactics" that gesture to the machine verifier how to fill in the gap, but more often than not, this is impossible.
In particular, informal proofs often move fluidly between different ways of representing a phenomenon, which often requires verbose specification of a translation in a formal proof description language. Natural language is much more fluid.
I heard Henk Barendregt talk of fortmal formal proofs being around six times as long as informal proofs. Harvey Friedman has claimed that ZF set theory with definitions and partial functions does better; I don't recall his estimate; see my answer in to the Is there a formal notion... question.
