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 statement3 of 3

More generally, they construct, for any mm and large nn, a set of nn points such that ⌊n2(m+1)⌋\lfloor \frac{n}{2(m+1)}\rfloor distances occur at least n+mn+m times.

FormalConjectures/ErdosProblems/756.leanErdos756.erdos_756.variants.bhowmick_general1 lineExact file
∀ (m : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∃ A, A.card = n ∧ n / (2 * (m + 1)) ≤ (Erdos756.richDistances A (n + m)).card
SolvedStatement only, no proof