---

Claim. Let $P$ be a set of $n$ points in the plane, let $u_1,\ldots,u_t$ be the distances it determines, and let $f(u_i)$ be the number of unordered pairs of points of $P$ at distance $u_i$. Proposition 2.2 of Guth and Katz bounds the number of ordered quadruples $(p_1,p_2,p_3,p_4)$ of points of $P$ with $|p_1-p_2|=|p_3-p_4|>0$ by $O(n^3\log n)$. Grouping the quadruples by the common distance, that number is $\sum_i (2f(u_i))^2$, so

$$\sum_i f(u_i)^2 \ll n^3\log n \ll_\epsilon n^{3+\epsilon}$$

for every $\epsilon>0$, which answers Problem 95 in the affirmative with a stronger bound than the one asked. The quadruple count is the intermediate result from which the paper's main theorem, that $n$ points determine $\gg n/\log n$ distinct distances, follows by the Cauchy–Schwarz inequality. The paper is carded at guth_2015_erdos_distinct_distance_problem_plane, whose annotation records the main theorem and the incidence bound behind it.

Acceptance. The paper is refereed: Larry Guth and Nets Hawk Katz, On the Erdős distinct distance problem in the plane, Ann. of Math. (2) 181 (2015), no. 1, 155–190; the preprint arXiv:1011.4105 was first posted on 2010-11-17. The site's curator, Thomas Bloom, marks the problem proved and credits Guth and Katz with the bound $\sum_i f(u_i)^2 \ll n^3\log n$ on the problem page; the site's export of 2026-09-04 records the label "PROVED (LEAN)".

Formalization. Boris Alexeev's repository of formalized Erdős problems holds a Lean development, added on 2026-08-17 and linked above at a pinned commit through its landing note, whose Lean file's header names Guth and Katz as informal authors and Codex and GPT-5.6 Sol as formal authors. Its theorem erdos_95 proves the $n^{3+\epsilon}$ bound the problem asks for through the Elekes–Sharir reduction and an $\epsilon$-loss bound on rich points obtained by polynomial partitioning, not from the $n^3\log n$ bound; the file also carries a separate $n^3\log n$ route that this theorem does not use. The statement erdos_95 in formal-conjectures, at the catalog's commit of 2026-09-20, is tagged research solved and points to that Lean file. This corpus has neither built nor audited the development, so no formalized evidence is listed.

The convex case. The site credits the case of a convex polygon to Altman (1963); the paper [[../library/distance_problems/altman_1963_problem_p_erdos/_index|carded in the library]] proves that a convex $n$-gon determines at least $\lfloor n/2\rfloor$ distinct distances and prints no statement about $\sum_i f(u_i)^2$, so that attribution has no claim page. The convex case is Problem 94, settled by [[problems/distance_problems/E0094/claims/1995_09_01_lefmann_thiele|Lefmann and Thiele]] with the bound $O(n^3)$.