9 points in a unit square with pairwise distances greater than $\frac12$ 
Consider a square with sides of length 1. Can we find 9 points in it such that the distance between every pair of points is strictly greater than $\frac12$?

We allow the points to be on the boundary of the square. The question arose in a conversation, and we are pretty confident that there is no such arrangement, and moreover the only configuration with pairwise distances at least half is the one where we take the vertices, the midpoints and the center.
Our thoughts
However, proving this seems nontrivial. An equivalent formulation is to look at the $\frac14$ blowup of the square and ask whether we can fit 9 circles with radius $\frac14$ in it or not. 
Moreover, the pigeonhole principle seems intuitively to be too weak for proving this, because if the shapes will be disjoint then each will have area around $\frac18$ and for, say, squares diameter half enforces area exactly $\frac18$, but we can't fit 8 such squares without gaps.

Assume there is a way for picking such $9$ points $P_1,\ldots,P_9$. Consider nine circles $\Gamma_i$ centered at $P_i$, with radius $\frac{1}{4}$. By our assumptions, these circles are disjoint and their union is contained in a square with side length $\frac{3}{2}=1+\frac{1}{4}+\frac{1}{4}$. The sum of the areas of our circles, $\frac{9\pi}{16}$, is less than the area of the augmented square, $\frac{9}{4}$, so the impossibility of such circle packing is not completely obvious. However, the optimal circle-packing-in-a-square is known for small numbers of circles, and that proves the impossibility of our arrangement.
