"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.