Erdős problem 655
Let be such that no circle whose centre is one of the contains three other points. Are there at least distinct distances determined between the , for some constant and all sufficiently large?
Sources
FormalConjectures/ErdosProblems/
655.lean
Retained formal statement
Let be such that no circle whose centre is one of the contains three other points. Are there at least distinct distances determined between the , for some constant and all sufficiently large?
In the spirit of related conjectures of Erdős and others, presumably some kind of assumption that the points are in general position (e.g. no three on a line and no four on a circle) was intended.
True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))), X.card = n → Erdos655.IsValid X → EuclideanGeometry.InGeneralPosition ↑X → (1 + c) * ↑n / 2 ≤ ↑(EuclideanGeometry.distinctDistances X)OpenStatement only, no proof