Erdős Problem 90: The unit distance problem

Reference: erdosproblems.com/90

The conjecture asks whether every set of $n$ points in $\mathbb{R}^2$ determines at most $n^{1 + O(1/\log\log n)}$ unit distances. It was disproved in May 2026: an internal model at OpenAI produced a construction beating the conjectured bound, with the proof digested and human-verified in two arXiv papers:

• W. Sawin, An explicit lower bound for the unit distance problem (2026), giving $u(n) \ge n^{1.014114}/C$ for infinitely many $n$;
• N. Alon, T. F. Bloom, W. T. Gowers, D. Litt, W. Sawin, A. Shankar, J. Tsimerman, V. Wang and M. Matchett Wood, Remarks on the disproof of the unit distance conjecture (2026), giving the qualitative form $u(n) \ge n^{1+\varepsilon}$ for some $\varepsilon > 0$.

This file records the main statement (erdos_90), the two constructive disproof variants, the logical implications between them, and the load-bearing reductions of Sawin's proof (sawin_lattice_reduction and sawin_totally_real_tower) as further benchmark challenges.

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.

theorem Erdos90.erdos_90.variants.polynomial_lower_bound : ∃ c > 0, {n : ℕ | ↑n ^ (1 + c) ≤ ↑(maxUnitDistances n)}.Infinite

Constructive form of the disproof. There is an absolute constant $c > 0$ such that infinitely many $n$ admit a configuration realising at least $n^{1+c}$ unit distances.

This is the qualitative content of Theorem 1.1 of Alon–Bloom–Gowers–Litt–Sawin–Shankar– Tsimerman–Wang–Matchett Wood, Remarks on the disproof of the unit distance conjecture (2026). An explicit bound $c \ge 0.014114$ is given by Sawin, An explicit lower bound for the unit distance problem (2026); see erdos_90.variants.sawin_explicit below.

theorem Erdos90.erdos_90.variants.sawin_explicit : {n : ℕ | ↑n ^ 1.014114 ≤ ↑(maxUnitDistances n)}.Infinite

Sawin's explicit exponent. The constructive disproof can be realised with $c \ge 0.014114$ (absorbing the implicit constant $C$ of Sawin's Theorem 1 into a slightly smaller exponent for all large enough $n$). Reference: Theorem 1 of Sawin, arXiv:2605.20579 (2026).

theorem Erdos90.erdos_90.variants.sawin_explicit_implies_polynomial_lower_bound : {n : ℕ | ↑n ^ 1.014114 ≤ ↑(maxUnitDistances n)}.Infinite → ∃ c > 0, {n : ℕ | ↑n ^ (1 + c) ≤ ↑(maxUnitDistances n)}.Infinite

Sawin's explicit bound implies the qualitative polynomial lower bound, by taking $c = 0.014114$.

theorem Erdos90.erdos_90.variants.polynomial_lower_bound_implies_erdos_90 : (∃ c > 0, {n : ℕ | ↑n ^ (1 + c) ≤ ↑(maxUnitDistances n)}.Infinite) → (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))

The polynomial lower bound implies the answer to Erdős 90 is False: a fixed positive exponent $c$ is incompatible with the conjectured $O(1 / \log \log n)$ growth.

theorem Erdos90.sawin_lattice_reduction (d : ℕ) (hd : 1 ≤ d) (R : ℝ) (hR : 2 ≤ R) (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin (2 * d)))) (π : ↥Λ →+ EuclideanSpace ℝ (Fin 2)) (hπ : Function.Injective ⇑π) (S : Finset ↥Λ) (hS_norm : ∀ v ∈ S, ‖↑v‖ ≤ 1) (hS_proj : ∀ v ∈ S, ‖π v‖ = 1) : ∃ (U : Finset (EuclideanSpace ℝ (Fin 2))), 0 < U.card ∧ (1 - 1 / R) ^ (2 * d) * ↑S.card * ↑U.card ≤ ↑(EuclideanGeometry.unitDistancePairsCount U)

Sawin's Lemma 2: lattice geometry of unit distances (Sawin, arXiv:2605.20579).

Let $d \ge 1$, $R \ge 2$, and suppose $\Lambda \subset \mathbb{R}^{2d}$ is a lattice equipped with an additive embedding $\pi : \Lambda \to \mathbb{R}^2$. Suppose $S \subseteq \Lambda$ is a finite set of "matching" vectors satisfying $\|v\| \le 1$ and $\|\pi v\| = 1$ for every $v \in S$. Then there is a finite point set $U \subset \mathbb{R}^2$ with unit-distance density at least $(1 - 1/R)^{2d}\,\#S$, i.e. $(1-1/R)^{2d}\,\#S\,\#U \le \#\{\text{unit pairs in } U\}$.

This pure geometry-of-numbers reduction is the elementary heart of the disproof.

theorem Erdos90.sawin_totally_real_tower : ∃ (rdBound : ℝ) (Q : Set ℕ), Q.Infinite ∧ (∀ q ∈ Q, Nat.Prime q ∧ q % 4 = 1) ∧ ∀ (N : ℕ), ∃ (F : Type) (x : Field F) (x_1 : CharZero F) (x_2 : NumberField F) (_ : NumberField.IsTotallyReal F), N ≤ Module.finrank ℚ F ∧ |↑(NumberField.discr F)| ^ (1 / ↑(Module.finrank ℚ F)) ≤ rdBound ∧ ∀ q ∈ Q, ∃ (factors : Finset (Ideal (NumberField.RingOfIntegers F))), factors.card = Module.finrank ℚ F ∧ ∀ p ∈ factors, p.IsMaximal ∧ ↑q ∈ p

Sawin's Lemmas 11–12 / Remarks Proposition 2.3: the totally real tower.

There exist $rdBound : \mathbb{R}$ and a single infinite set $Q$ of rational primes $q \equiv 1 \pmod 4$ such that for every $N$ one can find a totally real number field $F/\mathbb{Q}$ of degree $\ge N$ with bounded root discriminant $|disc F|^{1/[F:\mathbb{Q}]} \le rdBound$ in which every prime $q \in Q$ splits completely.

The load-bearing feature is the quantifier order: $Q$ is fixed before $F$, so the same primes split completely in fields of unbounded degree. (For a single fixed $F$, Chebotarev already gives infinitely many completely split primes $\equiv 1 \pmod 4$, so a per-field statement would be vacuous.) This uniform splitting in an unbounded tower is the key arithmetic input to the disproof. It is proved as Lemmas 11–12 of Sawin, arXiv:2605.20579, and as Proposition 2.3 of the Remarks paper, via the Golod–Shafarevich inequality for pro-$2$ groups together with the Hajir–Maire–Ramakrishna (2003) tower construction.

A "completely split" rational prime $q$ in $F$ is one for which $(q)$ is the product of exactly $[F:\mathbb{Q}]$ distinct maximal ideals.