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 statement3 of 8

The polynomial lower bound implies the answer to Erdős 90 is False: a fixed positive exponent $c$ is incompatible with the conjectured $O(1 / \log \log n)$ growth.

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

1(∃ c > 0, {n | ↑n ^ (1 + c) ≤ ↑(Erdos90.maxUnitDistances n)}.Infinite) →2  (False ↔3    ∃ O,4      ∃ (_ : O =O[Filter.atTop] fun n => 1 / Real.log (Real.log ↑n)),5        (fun n => ↑(Erdos90.maxUnitDistances n)) =ᶠ[Filter.atTop] fun n => ↑n ^ (1 + O n))

TestStatement only, no proof

Sources

Search problems.science