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
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.
∀ (n : ℕ), IsGreatest {x | ∃ A, ∃ (_ : A.IsIsosceles), A.ncard = x} sorryOpenStatement only, no proof