The smooth Poincaré conjecture in dimension 4

Let $X^4$ be a smooth $4$-manifold, and write $X^4 \simeq S^4$ when it is homeomorphic to $S^4$, while $X^4 \cong S^4$ means that it is diffeomorphic to $S^4$. An exotic $S^4$ is a smooth $4$-manifold homeomorphic but not diffeomorphic to $S^4$.

Smooth Poincaré conjecture in dimension 4. There are no exotic $S^4$'s; equivalently,

$$X^4 \simeq S^4 \qquad \implies \qquad X^4 \cong S^4.$$

This is presented as the most famous open question about exotic manifolds. It asks whether the topological $4$-sphere has a unique smooth structure.