Erdős problem 756 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

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.

Sources

Search problems.science