Asymptotic independence-ratio conjecture for finite unit-distance graphs

Let $f(n)$ denote the minimum independence number among $n$-vertex unit-distance graphs in the plane, and let $m_1(\mathbb R^2)$ be the supremum of the upper densities of measurable subsets of $\mathbb R^2$ containing no two points at distance $1$. Asymptotic independence-ratio conjecture.

$$\frac{f(n)}{n}=m_1(\mathbb R^2)+o(1).$$

Although the strict inequality $m_1(\mathbb R^2)<1/4$ is now solved, the problem of accurately estimating $f(n)/n$ remains wide open, including this conjectured asymptotic relation.