Because you
literally don't have to actually understand the proofs, just the definitions and proposition chain. Most of the code is going to be proving auxiliary lemmas or building up internal definitions that aren't needed to understand the final proposition. Then all you have to do is make sure the proof doesn't use any axioms and you're good. Being able to confidently do this is why proof assistants like Lean are really not just another programming language.
(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).