The Strong Lang Conjecture

Let $X$ be a variety defined over a number field $K$. A subvariety $\Sigma\subsetneqq X$ is proper when it is strictly smaller than $X$.

The Strong Lang Conjecture. If $X$ is of general type, then there exists a proper subvariety $\Sigma\subsetneqq X$ such that for any finite extension $K'$ of $K$,

$$\#(X\setminus\Sigma)(K')\;<\;\infty\,;$$

that is, the set of $K'$-rational points of $X$ lying outside of $\Sigma$ is finite.

This strengthens the Weak Lang Conjecture by requiring all rational points outside one proper subvariety to be finite after every finite extension. Its general status remains open.