Erdős problem 503
What is the size of the largest such that every three points from determine an isosceles triangle? That is, for any three points , , from , at least two of the distances , , are equal.
Sources
FormalConjectures/ErdosProblems/
503.lean
Retained formal statement
The best upper bound known in general is due to Blokhius [Bl84] who showed that
[Bl84] Blokhuis, A., Few-distance sets. (1984), iv+70.
∀ (n m : ℕ), m ∈ {x | ∃ A, ∃ (_ : A.IsIsosceles), A.ncard = x} → m ≤ (n + 2).choose 2SolvedStatement only, no proof