many of the things that look like inefficiencies are actually trading off small local gains for large global gains

This is an interesting hypothesis, and one I wasn't thinking of. But hard to measure!

For instance, MIRI repeatedly brings up Paul's probabilistic metamathematics as an important piece of research progress produced by MIRI.

Out of curiosity, what gives you that impression? I tend to cite it because it is (along with the Lobian cooperation stuff) among the most important results to come out of MIRI's first couple workshops, not because I can already tell whether it's an important breakthrough in mathematical logic in general.

As for the purpose and relevance of the Lobian obstacle work, it seems like there might still be a failure of communication there. Since you and Eliezer and I discussed this at length and there still seems to be an unbridged gap, I'm not sure which thing I can say to bridge the gap. Maybe this quote from Paul?

No one thinks that the world will be destroyed because people built AI's that couldn't handle the Lobian obstruction. That doesn't seem like a sensible position, and I think Eliezer explicitly disavows it in the writeup. The point is that we have some frameworks for reasoning about reasoning. Those formalisms don't capture reflective reasoning, i.e. they don't provide a formal account of how reflective reasoning could work in principle. The problem Eliezer points to is an obvious problem that any consistent framework for reflective reasoning must resolve.

Working on this problem directly may be less productive than just trying to understand how reflective reasoning works in general---indeed, folks around here definitely try to understand how reflective reasoning works much more broadly, rather than focusing on this problem. The point of this post is to state a precise problem which existing techniques cannot resolve, because that is a common technique for making progress.

Another example would be decision theory of modal agents. I also won't take the time to treat this in detail, but will simply note that this work studies a form of decision theory that MIRI itself invented, and that no one else uses or studies.

In the OP I actually gave program equilibrium as an example of new theoretical progress that opens up new lines of inquiry, e.g. the modal agents work (though of course there are other pieces contributing to modal agents, too). So yeah, I don't think the modal agents work is an example of inefficiency.

The examples I gave in the OP for apparent inefficiency in decision theory research was philosophy's failure to formulate a reliabilist metatheory of instrumental rationality until 2013, even though reliabilist theories of epistemic rationality have been popular since the late 1960s, and also the apparently slow uptake of causal Bayes nets in the causal decision theory world.