If it really is formalized, it seems like the exact ideas would be able to be translated to and from any other sufficiently capable language without gaining or losing anything.
Then when a translation exists the proofs can blow up in size to where you lose feasibility and understandability even tho they are technically still proofs.
Regardless of all that, I wasn't even bringing up 1lab because of the choice of language or type theory. I bring it up as an example of a pro-human way of presenting formalization.