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.
 A: The answer is NO.
This was first proved by J.Schaer in a paper "The densest packing of 9 circles in a square" appeared in Canadian Mathematical Bulletin, 1964. An online copy is available on CMB.
In that paper, Schaer have shown:

For any nine points $P_i (1 \le i \le 9)$ of a closed unit square,
  $$\min_{1\le i < j \le 9} d(P_i,P_j) \le \frac12$$
  and that equality holds only when $P_i$ lie on a $3\times 3$ grid of spacing $\frac12$.

The basic idea goes as follow:
Let's say we are given $9$ points $P_i (1 \le i \le j)$ on the unit square 
whose pairwise distances $d(P_i,P_j) \ge \frac12$. Split the unit square into $9$ squares $Q_{0i}, (1 \le i \le 9)$ of side $s_0 = \frac13$. Since the diameter of these squares is $\frac{\sqrt{2}}{3} < \frac12$ and there are $9$ squares for $9$ points, each square $Q_{0i}$ contains exactly one $P_i$. 
Schaer then outline a procedure to restrict each $P_i$ further to another set of small squares $P_i \in Q_{i1} \subset Q_{0i}$ with side $s_1 < s_0$. This procedure can be repeated and at the end he obtained $9$ sequences of squares
such that
$$P_i \in \cdots \subset Q_{ni} \subset Q_{n-1i} \subset \cdots \subset Q_{1i} \subset Q_{0i}$$
with sides $s_0 > s_1 > s_2 > \cdots$ and $s_n \to 0$ as $n \to \infty$.
The limiting configuration of $P_i$ is unique and the nine points lie on a $3 \times 3$ grid for side $\frac12$.
This is as far as I can summarize the basic idea. For more details, please refer to the paper in above link. It is pretty elementary and easy to understand.
A: 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.
