Erdős problem 90

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

Sources

The source's own material, retained exactly.

9 retained statements36c6d0fef71a

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