Wiki
Wiki

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 A⊂R2A\subset \mathbb{R}^2 be a set of nn points. Can there be ≫n\gg n many distinct distances each of which occurs for more than nn many pairs from AA?

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 nn points in the plane can determine ≫n\gg n distinct distances each occurring for more than nn pairs. The answer is yes, by the construction on the accepted claim page: for every nn, a set of nn points with ⌊n/4⌋\lfloor n/4\rfloor distances each occurring at least n+1n+1 times, and for every m≥1m\geq1 and every nn, nn points with ⌊n/(2(m+1))⌋\lfloor n/(2(m+1))\rfloor distances each occurring at least n+mn+m 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 nn times, is Problem 132 and is not settled here; Hopf and Pannwitz [HoPa34] bound the largest distance's multiplicity by nn. Clemen, Dumitrescu and Liu [CDL25] (Acta Math. Hungar. 177 (2025)) add that the n×n\sqrt n\times\sqrt n grid has at least nc/log⁡log⁡nn^{c/\log\log n} distances of multiplicity at least n1+c/log⁡log⁡nn^{1+c/\log\log n} for some c>0c>0. This is a result in a different regime, superlinear multiplicity for only no(1)n^{o(1)} distances, which [CDL25] present as an improvement on Bhowmick's bound for multiplicity n+mn+m with mm large; it is not part of the question, which asks for ≫n\gg n 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.