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

Browse retained paths and inspect the exact material available for this Problem.

9 retained statements2415f78e850a

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(1loglogn)n^{1+O(\frac{1}{\log\log n})} many pairs which are distance 11 apart?

This was [disproved](https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf) 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
FalseO,    ∃ (_ : O =O[Filter.atTop] fun n => 1 / Real.log (Real.logn)),      (fun n => ↑(Erdos90.maxUnitDistances n)) =ᶠ[Filter.atTop] fun n => ↑n ^ (1 + O n)
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page