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

The source's own material, retained exactly.

9 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

90.lean

Retained formal statement4 of 8

Sawin's explicit exponent. The constructive disproof can be realised with c≥0.014114c \ge 0.014114 (absorbing the implicit constant CC of Sawin's Theorem 1 into a slightly smaller exponent for all large enough nn). Reference: Theorem 1 of Sawin, arXiv:2605.20579 (2026).

FormalConjectures/ErdosProblems/90.leanErdos90.erdos_90.variants.sawin_explicit1 lineExact file
{n | ↑n ^ 1.014114 ≤ ↑(Erdos90.maxUnitDistances n)}.Infinite
SolvedStatement only, no proof