Erdős problem 90 · problems.science

Conjectured upper bound on how many pairs among $n$ 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

FormalConjectures/ErdosProblems/

90.lean

Retained formal statement5 of 8

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

FormalConjectures/ErdosProblems/90.leanErdos90.erdos_90.variants.sawin_explicit_implies_polynomial_lower_bound2 linesExact file

1{n | ↑n ^ 1.014114 ≤ ↑(Erdos90.maxUnitDistances n)}.Infinite →2  ∃ c > 0, {n | ↑n ^ (1 + c) ≤ ↑(Erdos90.maxUnitDistances n)}.Infinite

TestStatement only, no proof