If anything, it's a relatively straightforward way to do what amounts to publishable work in mathematics. Besides the obvious point of being able to claim "I've dotted all the i's and crossed all the t's", formalized proofs are often more elegant than the original they're based on because refactoring a proof to be simpler, more general etc. and checking that it still goes through is comparatively easy - and obviously, mathematicians are interested in that.
The refactoring idea is interesting because I can imagine "proof compression" creating a less readable proof too, similarly to how a code one liner can be harder to read.
