Erdős problem 756
Let be a set of points. Can there be many distinct distances each of which occurs for more than many pairs from ?
Sources
FormalConjectures/ErdosProblems/
756.lean
Retained formal statement
Let be a set of points. Can there be many distinct distances each of which occurs for more than many pairs from ?
The answer is yes: Bhowmick [Bh24] constructs a set of points in such that distances occur at least times.
True ↔ (fun n => ↑n) =O[Filter.atTop] fun n => ↑(Erdos756.maxRichDistances n)SolvedStatement only, no proof