Erdős problem 93

If $n$ distinct points in $\mathbb{R}^2$ form a convex polygon then they determine at least $\lfloor \frac{n}{2}\rfloor$ distinct distances.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

93.lean

Retained formal statement1 of 1

If $n$ distinct points in $\mathbb{R}^2$ form a convex polygon then they determine at least $\lfloor \frac{n}{2}\rfloor$ distinct distances.

Solved by Altman [Al63].

FormalConjectures/ErdosProblems/93.leanErdos93.erdos_932 linesExact file

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

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.