Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 756
claims/: The 1 claim page of Problem 756, one per claimant's result; the problem's standing derives from them.
Statement. Let be a set of points. Can there be many distinct distances each of which occurs for more than many pairs from ?
Status. PROVED (LEAN). The site marks the problem proved, crediting Bhowmick's construction, and flags a Lean formalization of his proof; see the claim page.
Source. erdosproblems.com/756, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #756, https://www.erdosproblems.com/756.
References.
- [Bh24] K. Bhowmick, A problem of Erdős about rich distances. arXiv:2407.01174 (2024). Published as: A note on a problem of Erdős about rich distances. Studia Sci. Math. Hungar. 62 (2025), no. 1, 89-94.
- [CDL25] F. Clemen, A. Dumitrescu, and D. Liu, On multiplicities of interpoint distances. arXiv:2505.04283 (2025). Acta Math. Hungar. 177 (2025), 231-245.
- [Er97b] Erdős, Paul, Some old and new problems in various branches of combinatorics. Discrete Math. 165/166 (1997), 227-231.
- [ErPa90] Erdős, Paul and Pach, János, Variations on the theme of repeated distances. Combinatorica 10 (1990), 261-269.
- [HoPa34] Hopf, H. and Pannwitz, E., Aufgabe 167. Jber. Deutsch. Math. Verein. (1934), 114.
Formalization. Statement in formal-conjectures. A Lean formalization of Bhowmick's proof by Aristotle (Harmonic), announced on the site's discussion thread in March 2026 and held in Wouter van Doorn's and Boris Alexeev's repositories, is a formalization link on Bhowmick's claim page; this corpus has not built it, and it is not native Lean coverage.
Current assessment
Proved. The site formulation above asks whether points in the plane can determine distinct distances each occurring for more than pairs. The answer is yes, by the construction on the accepted claim page: for every , a set of points with distances each occurring at least times, and for every and every , points with distances each occurring at least times. The result is refereed (Studia Sci. Math. Hungar. 62 (2025)) and the site's curator credits it; a Lean formalization of the proof by Aristotle exists and is linked from the claim page, but has not been built here. The standing derives from that claim page.
The question is the weaker of two asked by Erdős and Pach [ErPa90] and restated in [Er97b]: the stronger one, whether every distance other than the largest can occur more than times, is Problem 132 and is not settled here; Hopf and Pannwitz [HoPa34] bound the largest distance's multiplicity by . Clemen, Dumitrescu and Liu [CDL25] (Acta Math. Hungar. 177 (2025)) add that the grid has at least distances of multiplicity at least for some . This is a result in a different regime, superlinear multiplicity for only distances, which [CDL25] present as an improvement on Bhowmick's bound for multiplicity with large; it is not part of the question, which asks for such distances. Search scope (2026-10-07): the site's problem page and discussion thread, the arXiv and publisher records of [Bh24] and [CDL25], and the Lean repositories named above; no forum proof claim, release item or lead names the problem.
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.