Erdős problem 502 · problems.science

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

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

502.lean

Retained formal statement1 of 1

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

Asked to Erdős by Coxeter. Bannai, Bannai, and Stanton [BBS83] have proved that $\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 $\binom{n+1}{2}$ follows from the construction of Alweiss (see [503]).

FormalConjectures/ErdosProblems/502.leanErdos502.erdos_5022 linesExact file

1∀ (n : ℕ) (A : Set (EuclideanSpace ℝ (Fin n))),2  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.

Sources

Search problems.science