Erdős problem 1082

Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line. Must there exist a single point from which there are at least $\lfloor n/2\rfloor$ distinct distances?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1082.lean

Retained formal statement1 of 2

Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line. Does $A$ determine at least $\lfloor n/2\rfloor$ distinct distances?

FormalConjectures/ErdosProblems/1082.leanErdos1082.erdos_1082.parts.i3 linesExact file

1True ↔2  ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))),3    EuclideanGeometry.NonTrilinear ↑A → A.card / 2 ≤ EuclideanGeometry.distinctDistances A

OpenStatement only, no proof