Problem 95

Let $x_1,\ldots,x_n\in\mathbb{R}^2$ determine the set of distances $\{u_1,\ldots,u_t\}$ . Suppose $u_i$ appears as the distance between $f(u_i)$ many pairs of points. Then for all $\epsilon>0$

\sum_i f(u_i)^2 \ll_\epsilon n^{3+\epsilon}.

Source: erdosproblems.com/95

Geometry
Convexity
Distances

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

Proved. The site's export of 2026-09-04 records the label "PROVED (LEAN)". The proof is Guth and Katz's bound $\sum_i f(u_i)^2\ll n^3\log n$ , recorded on its claim page (Guth and Katz, 2010); the Lean qualification refers to a development in Boris Alexeev's repository that this corpus has neither built nor audited (see Formalization). The site's attribution of the convex case to Altman has no claim page, since his paper prints no statement about the sum (see the claim page and the card below); the convex case is Problem 94.

Al63: Altman, E., On a problem of P. Erdős. Amer. Math. Monthly 70 (1963), no. 2, 148--157, JSTOR 2312883. Library home: Altman 1963. Its printed statements concern the number of distinct distances of a convex polygon, at least $\lfloor n/2\rfloor$ (the Theorem, p. 149); it prints no statement about $\sum_i f(u_i)^2$ , so the site's convex-polygon attribution to it is recorded on its card as an observation.
GuKa15: Guth, Larry and Katz, Nets Hawk, On the Erdős distinct distances problem in the plane. Ann. of Math. (2) (2015), 155-190.

Problem 95

Status

Proof claims

Discussion