\documentclass[11pt]{scrartcl}
\usepackage{evan}
\begin{document}
\title{IMO 1987/5}
\subtitle{Evan Chen}
\author{Twitch Solves ISL}
\date{Episode 117}
\maketitle
\section*{Problem}
Is it possible to put $1987$ points in the Euclidean plane
such that the distance between each pair of points is irrational and
each three points determine a non-degenerate triangle with rational area?
\section*{Video}
\href{https://www.youtube.com/watch?v=MQizW3_nrZE&list=PLi6h8GM1FA6yHh4gDk_ZYezmncU1EJUmZ}{\texttt{https://youtu.be/MQizW3\_nrZE}}
\section*{External Link}
\url{https://aops.com/community/p366548}
\newpage
\section*{Solution}
Note that any triangle with vertices which are lattice points has rational area.
So we'd be done if we could prove:
\begin{claim*}
Given a finite set $S$ of lattice points, we can add one lattice point $P$
such that $P$ is irrational distance from every point in $S$.
\end{claim*}
\begin{proof}
Suppose $S$ lies inside $[1,n] \times [1,n]$.
Let $a^2+b^2=c^2$ by a primitive Pythagorean triple
with the additional property that $a/b \neq x/y$ for any $(x,y) \in S$;
this is possible there are infinitely many primitive Pythagorean triples.
Consider large $R$; I claim that $P = \left( aR, bR \right)$ is okay
if $R$ is sufficiently large.
The squared distance from $P$ to a point $(u,v)$ is
\[ D = \left( aR-u \right)^2 + \left( bR-v \right)^2
= (cR)^2 - 2(au+bv)R + (u^2+v^2) \]
So for this to be square, it must be inside the set
\[ D \in \{(5R-(a+b)n)^2, (5R-(a+b)n+1)^2, \dots, (5R+2n)^2 \}. \]
In other words, if $R$ is large enough, then $D$ is not a square
unless $D$ is actually identically the square of a polynomial in $R$.
For that to be the case, we would need
\[ D = \left( cR - \sqrt{u^2+v^2} \right)^2 \]
which would only happen if
\[ c\sqrt{u^2+v^2} = au+bv
\implies 0 = c^2(u^2+v^2) - (au+bv)^2 = (bu-av)^2 \]
which doesn't happen because we assured $a/b \neq u/v$.
Hence for each $(u,v) \in S$, there exists a constant $C_{u,v}$
for which $R > C_{u,v}$ guarantees $P$ is irrational distance from $(u,v)$.
Take the max of these finitely many constants to finish.
\end{proof}
\end{document}