Skip to content

Erdős problem 756

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?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

756.lean

Retained formal statement1 of 3

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?

The answer is yes: Bhowmick [Bh24] constructs a set of nn points in R2\mathbb{R}^2 such that ⌊n4⌋\lfloor\frac{n}{4}\rfloor distances occur at least n+1n+1 times.

FormalConjectures/ErdosProblems/756.leanErdos756.erdos_7561 lineExact file
True ↔ (fun n => ↑n) =O[Filter.atTop] fun n => ↑(Erdos756.maxRichDistances n)
SolvedStatement only, no proof