Planar distinct distances and unit-distance bounds

Proves the weak pinned Erdős distance conjecture: for every fixed ε > 0, all but o(n) points of any n-point planar set determine at least n^{1-\varepsilon} distinct nonzero distances. A complementary theorem bounds the number of unit-distance pairs by O(n^{4/3-\delta}) for an absolute δ > 0. (Lean)

Manuscripts (2)

The weak pinned planar distance theorem

September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:The-weak-pinned-planar-distance-theorem-September-23-2026}

We prove the weak pinned Erdős distinct-distance conjecture. For every fixed ε > 0, all but o(n) points of any n-point planar set determine at least n^{1-\varepsilon} distinct nonzero distances.

A power saving for planar unit distances

September 23, 2026 · source · cite as \cite{OAI:A-power-saving-for-planar-unit-distances-September-23-2026}

We prove a power saving for the planar unit-distance problem: for some absolute \beta\lt 4/3, every set of n points in the Euclidean plane determines O(n^\beta) unordered pairs at unit distance.

Result 167 · Combinatorics. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Agora members.