The PFA conjecture

The theories involved are ZFC and PFA, and ZFC with a supercompact cardinal.

PFA conjecture. The following theories are equiconsistent:

$$\begin{array}{ll} \text{ZFC+PFA},\\ \text{ZFC+“there is a supercompact cardinal”}. \end{array}$$

The reverse consistency implication is a theorem due to Baumgartner; the forward direction is a central target of descriptive inner model theory and remains open.