Erdős problem 756

Let $A\subset \mathbb{R}^2$ be a set of $n$ points. Can there be $\gg n$ many distinct distances each of which occurs for more than $n$ many pairs from $A$ ?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

756.lean

Retained formal statement2 of 3

Bhowmick [Bh24] constructs a set of $n$ points in $\mathbb{R}^2$ such that $\lfloor\frac{n}{4}\rfloor$ distances occur at least $n+1$ times.

FormalConjectures/ErdosProblems/756.leanErdos756.erdos_756.variants.bhowmick1 lineExact file

1∀ (n : ℕ), ∃ A, A.card = n ∧ n / 4 ≤ (Erdos756.richDistances A (n + 1)).card

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.