Skip to content

Erdős problem 502

What is the size of the largest A⊆RnA\subseteq \mathbb{R}^n such that there are only two distinct distances between elements of AA? That is, #{∣x−y∣:x≠y∈A}=2.\# \{ \lvert x-y\rvert : x\neq y\in A\} = 2.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

502.lean

Retained formal statement1 of 1

What is the size of the largest A⊆RnA\subseteq \mathbb{R}^n such that there are only two distinct distances between elements of AA? That is, #{∣x−y∣:x≠y∈A}=2.\# \{ \lvert x-y\rvert : x\neq y\in A\} = 2.

Asked to Erdős by Coxeter. Bannai, Bannai, and Stanton [BBS83] have proved that ∣A∣≤(n+22).\lvert A\rvert \leq \binom{n+2}{2}. A simple proof of this upper bound was given by Petrov and Pohoata [PePo21].

The exact maximum is not known in general: a lower bound of (n+12)\binom{n+1}{2} follows from the construction of Alweiss (see [503]).

FormalConjectures/ErdosProblems/502.leanErdos502.erdos_5022 linesExact file
∀ (n : ℕ) (A : Set (EuclideanSpace ℝ (Fin n))),  A.Finite → {d | ∃ x ∈ A, ∃ y ∈ A, x ≠ y ∧ dist x y = d}.ncard = 2 → A.ncard ≤ (n + 2).choose 2
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.