Erdős Problem a Daythe open tracker

Erdős Problem #95

PROVED LEANdatabase updated 2026-08-24

The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

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}.\] The case when the points determine a convex polygon was solved by Altman [Al63]. Note it is trivial that \(\sum f(u_i)=\binom{n}{2}\). Solved by Guth and Katz [GuKa15] who proved the upper bound \[\sum_i f(u_i)^2 \ll n^3\log n.\] See also [94](https://www.erdosproblems.com/94).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/95.
Prize$500
Topicsgeometry, convex, distances
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/95
NOBODY HAS SENT US AN ATTEMPT YET

If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.