Skip to content

Erdős problem 502

Start work

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.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/502.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:502
  • PLBY Lean proofsErdosProblems.Erdos502

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry