---

Claim. The answer to Problem 756 is yes. Krishnendu Bhowmick, A note on a problem of Erdős about rich distances, Studia Sci. Math. Hungar. 62 (2025), no. 1, 89--94; posted as arXiv:2407.01174, A problem of Erdős about rich distances, on 1 July 2024. For every $n$ the paper constructs a set of $n$ points in $\mathbb{R}^2$ in which $\lfloor n/4\rfloor$ distinct distances each occur for at least $n+1$ pairs of points, so $\gg n$ distances occur more than $n$ times, as the question asks (Theorem 1.1). More generally, for every $m\geq1$ and every $n$ it gives $n$ points with $\lfloor n/(2(m+1))\rfloor$ distances each occurring at least $n+m$ times (Theorem 1.2, vacuous for $n<m+3$). The witnesses are built from regular polygons. A regular $(m+1)$-gon has $\lfloor m/2\rfloor$ distances each occurring $m+1$ times (Claim 2.1). For odd $n=2m+1$ the polygon is rotated about one of its vertices, and the two copies share only that vertex, so they have $2m+1=n$ points and each of the $\lfloor m/2\rfloor=\lfloor n/4\rfloor$ distances occurs $2(m+1)=n+1$ times; for even $n=2m$ the polygon is reflected in one of its edges, the two copies share only that edge's two endpoints, so they have $2m=n$ points and each of those distances occurs at least $2(m+1)-1=n+1$ times, the shared edge being counted once. Theorem 1.2 iterates the same two moves on a regular $(k+2)$-gon, $r-2$ rotations about a fixed vertex and $m+2-r$ reflections in edges, where $n=(m+1)k+r$ with $2\leq r\leq m+2$. The source card is Bhowmick 2024. The question comes from Erdős and Pach, who asked it in the stronger form of whether every distance other than the largest can occur more than $n$ times; by Hopf and Pannwitz the largest distance occurs at most $n$ times, and that stronger form is a separate problem.

Acceptance. The result is refereed: it appeared in Studia Scientiarum Mathematicarum Hungarica. The site's curator, Thomas Bloom, marks the problem proved and credits Bhowmick's construction; the site labels the problem PROVED (LEAN) (export of 2026-09-04).

Formalization. The site's label carries a Lean marker. Wouter van Doorn announced on the site's discussion thread on 15 March 2026 that Bhowmick's proof had been formalized by Aristotle (Harmonic), and posted the file in van Doorn's own repository, linked above at its commit of that day. Boris Alexeev's repository of formalized Erdős problems holds the same development, linked above at a pinned commit; its header declares it a Lean formalization of a solution to Problem 756 with Bhowmick as informal author and Aristotle and van Doorn as formal authors. Its theorem Erdos756.erdos_756 states that for every $n$ there is an $n$-point set of complex numbers and a set of $\lfloor n/4\rfloor$ of its distances each realized by at least $n+1$ unordered pairs, and the file prints its axioms as propext, Classical.choice and Quot.sound. The formal-conjectures statement file for the problem (last changed 2026-09-18) records this proof, through a formal_proof attribute pointing at the unpinned src/v4.29.1 copy in Alexeev's repository, against its variant erdos_756.variants.bhowmick, which states the $\lfloor n/4\rfloor$ construction; its main statement and its general variant carry no proof. This corpus has not built the file or audited its statement, so it is a link here and not formalized evidence.