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.

"sufficiently capable" is doing an insane amount of heavy lifting here. Like you can only interpret a theory into another one if the target is at least as strong as the source and even then "to and from" is a MUCH stronger condition that most pairs of theories do not satisfy.

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.