Skip to content

Erdős problem 958

Let A⊂R2A\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

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

958.lean

Retained formal statement1 of 1

Let A⊂R2A\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=n−1k=n-1 and {f(di)}={n−1,…,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 A ∨ Erdos958.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.