Erdős Problem #756
PROVED LEANdatabase updated 2026-03-15
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).
The distances determined by `A` which occur for at least `k` many pairs of points of `A`.
The largest number of distinct distances that a set of `n` points in \(\mathbb{R}^2\) can determine, each of which occurs for more than `n` many pairs of points of the set.
Let \(A\subset \mathbb{R}^2\) be a set of \(n\) points. Can there be \(\gg n\) many distinct distances each of which occurs for more than \(n\) many pairs from \(A\)? The answer is yes: Bhowmick [Bh24] constructs a set of \(n\) points in \(\mathbb{R}^2\) such that \(\lfloor\frac{n}{4}\rfloor\) distances occur at least \(n+1\) times.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/756.Prizenone
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/756
Attempts
submit one →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.