Skip to content

Erdős problem 958

Let AR2A\subset \mathbb{R}^2 be a finite set of size nn, and let {d1,,dk}\{d_1,\ldots,d_k\} be the set of distances determined by AA. Let f(d)f(d) be the multiplicity of dd, that is, the number of unordered pairs from AA of distance dd apart.

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

958.lean

Retained formal statement1 of 1

Let AR2A\subset \mathbb{R}^2 be a finite set of size nn, and let {d1,,dk}\{d_1,\ldots,d_k\} be the set of distances determined by AA. Let f(d)f(d) be the multiplicity of dd, that is, the number of unordered pairs from AA of distance dd apart.

Is it true that k=n1k=n-1 and {f(di)}={n1,,1}\{f(d_i)\}=\{n-1,\ldots,1\} if and only if AA 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 11, together with the centre, are also an example.

FormalConjectures/ErdosProblems/958.leanErdos958.erdos_9587 linesExact file
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 AErdos958.IsEquidistantOnCircle 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.

Search problems.science

Find a Problem, Result, source, or page