Yes it compresses the proofs but still "Sol had generated 1.2 million lines of Lean code in the three weeks that it had worked on the project". I mean how do you even verify that?
(That's not to say there's no value to making the proof themselves nicer--compilation time and reusability can actually be a really big deal in formalized mathematics!--but it's way less important than it is in software).