Problem 90

Does every set of $n$ distinct points in $\mathbb{R}^2$ contain at most $n^{1+O(1/\log\log n)}$ many pairs which are distance 1 apart?

Source: erdosproblems.com/90

Geometry
Distances

Wiki page

Status

SolvedDisproved

An accepted solution exists. The statement is false.

Disproved. The site's export of 2026-09-04 labels the problem "DISPROVED (LEAN)" (page last edited 20 May 2026); the corpus has built none of the Lean developments behind the Lean marker (see "Formalization and the Lean label" below).

Er82e: Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59-79.
Er83c: Erdős, Paul, Combinatorial problems in geometry. Math. Chronicle (1983), 35-54.
Er85: Erdős, P., Problems and results in combinatorial geometry. Discrete geometry and convexity (New York, 1982) (1985), 1-11.
Er94b: Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.
SST84: Spencer, J. and Szemerédi, E. and Trotter, Jr., W., Unit distances in the Euclidean plane. Graph theory and combinatorics (Cambridge, 1983) (1984), 293-303.
Sz16: Szemerédi, Endre, Erdős's unit distance problem. Open problems in mathematics (2016), 459-477.
OpenAI26: OpenAI, Planar Point Sets with Many Unit Distances. Unnumbered 18-page technical report (2026).
ABGLSSTWW26: N. Alon, T. F. Bloom, W. T. Gowers, D. Litt, W. Sawin, A. Shankar, J. Tsimerman, V. Wang, and M. Matchett Wood, Remarks on the disproof of the unit distance conjecture, arXiv:2605.20695v1 (2026).
Sa26: W. Sawin, An explicit lower bound for the unit distance problem, arXiv:2605.20579v1 (2026).
Em26: M. T. M. Emmerich, Optimizing explicit unit-distance lower-bound certificates, arXiv:2606.03419v5 [math.OC] (2026).
Tori26: Integral points on norm-one tori and the Erdős unit-distance exponent, 13-page manuscript with no author line, hosted at www-cdn.anthropic.com, retrieved (2026).

Problem 90

Status

Proof claims

Discussion