Erdős problem 90
Conjectured upper bound on how many pairs among points in the plane can be exactly one unit apart.
Sources
FormalConjectures/ErdosProblems/
90.lean
Retained formal statement
Sawin's explicit exponent. The constructive disproof can be realised with (absorbing the implicit constant of Sawin's Theorem 1 into a slightly smaller exponent for all large enough ). Reference: Theorem 1 of Sawin, [arXiv:2605.20579](https://arxiv.org/abs/2605.20579) (2026).
{n | ↑n ^ 1.014114 ≤ ↑(Erdos90.maxUnitDistances n)}.InfiniteSolvedStatement only, no proof