Skip to content

Erdős problem 90

Start work

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

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

FormalConjectures/ErdosProblems/90.leanErdos90.erdos_90.variants.polynomial_lower_bound_implies_erdos_905 linesExact file
(∃ c > 0, {n | ↑n ^ (1 + c) ≤ ↑(Erdos90.maxUnitDistances n)}.Infinite) →  (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))
TestStatement only, no proof