Skip to content

Erdős problem 90

Conjectured upper bound on how many pairs among nn points in the plane can be exactly one unit apart.

Sources

The source's own material, retained exactly.

9 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

90.lean

Retained formal statement1 of 8

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

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

FormalConjectures/ErdosProblems/90.leanErdos90.erdos_904 linesExact file
False ↔  ∃ O,    ∃ (_ : O =O[Filter.atTop] fun n => 1 / Real.log (Real.log ↑n)),      (fun n => ↑(Erdos90.maxUnitDistances n)) =ᶠ[Filter.atTop] fun n => ↑n ^ (1 + O n)
SolvedStatement only, no proof