Erdős problem 958
Let be a finite set of size , and let be the set of distances determined by . Let be the multiplicity of , that is, the number of unordered pairs from of distance apart.
Sources
FormalConjectures/ErdosProblems/
958.lean
Let be a finite set of size , and let be the set of distances determined by . Let be the multiplicity of , that is, the number of unordered pairs from of distance apart.
Is it true that and if and only if is a set of equidistant points on a line or a circle?
Erdős conjectured that the answer is no, and other such configurations exist.
This was proved by Clemen, Dumitrescu, and Liu [CDL25], who observed that equidistant points on a short circular arc on a circle of radius , together with the centre, are also an example.
False ↔ ∀ (n : ℕ) (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → (EuclideanGeometry.distanceSet A).card = n - 1 ∧ Finset.image (EuclideanGeometry.distanceMultiplicity A) (EuclideanGeometry.distanceSet A) = Finset.Icc 1 (n - 1) → Erdos958.IsEquidistantOnLine A ∨ Erdos958.IsEquidistantOnCircle A