Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 95

claims/: The 1 claim page of Problem 95, one per claimant's result; the problem's standing derives from them.

Statement. 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}.

Status. 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 [[problems/distance_problems/E0095/claims/2010_11_17_guth_katz|its claim page]]; 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.

Source. erdosproblems.com/95, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #95, https://www.erdosproblems.com/95.

References.

[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_problem_p_erdos. 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.

Formalization. Statement in formal-conjectures, which at the linked commit of 2026-09-20 tags erdos_95 research solved with a pointer to a Lean proof in Boris Alexeev's repository, linked at a pinned commit on the [[problems/distance_problems/E0095/claims/2010_11_17_guth_katz|Guth–Katz claim page]]; this corpus has neither built nor audited it.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (7)

Guth and Katz's bound on repeated distances problems/distance_problems/E0095/claims Distance Problems distance_problems/altman_1963_problem_p_erdos Theorem (p. 149): a plane convex n-gon determines at least [n/2] distinct distances On the Erdős distinct distance problem in the plane Proposition 2.2 (p. 160): N plane points have ≲ N³ log N distance quadruples

Graph