Erdős Problem 90: The unit distance problem

Reference: erdosproblems.com/90

noncomputable def Erdos90.unitDistanceCounts (n : ℕ) : Set ℕ

The set of all possible numbers of unit distances for a configuration of $n$ points.

Equations

• Erdos90.unitDistanceCounts n = {x : ℕ | ∃ (points : Finset (EuclideanSpace ℝ (Fin 2))) (_ : points.card = n), EuclideanGeometry.unitDistancePairsCount points = x}

theorem Erdos90.unitDistanceCounts_BddAbove (n : ℕ) : BddAbove (unitDistanceCounts n)

This lemma confirms that the set of possible unit distance counts is bounded above, which ensures that taking the supremum (sSup) is a well-defined operation. The trivial upper bound is the total number of pairs of points, $\binom{n}{2}$.

noncomputable def Erdos90.maxUnitDistances (n : ℕ) : ℕ

The maximum number of unit distances determined by any set of $n$ points in the plane. This function is often denoted as $u(n)$ in combinatorics.

Equations

• Erdos90.maxUnitDistances n = sSup (Erdos90.unitDistanceCounts n)

theorem Erdos90.erdos_90 : False ↔ ∃ (O : ℕ → ℝ) (_ : O =O[Filter.atTop] fun (n : ℕ) => 1 / Real.log (Real.log ↑n)), (fun (n : ℕ) => ↑(maxUnitDistances n)) =ᶠ[Filter.atTop] fun (n : ℕ) => ↑n ^ (1 + O n)

Does every set of $n$ distinct points in $\mathbb{R}^2$ contain at most $n^{1+O(\frac{1}{\log\log n})}$ many pairs which are distance $1$ apart?

This was disproved by an internal model at OpenAI, which constructed (for infinitely many $n$) a set $P$ of $n$ points in $\mathbb{R}^2$ such that the number of unit distance pairs in $P$ is at least $n^{1+c}$, where $c > 0$ is an absolute constant.