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
When , the answer is 8 (due to Croft [Cr62]).
[Cr62] Croft, H. T., -point and -point configurations in -space. Proc. London Math. Soc. (3) (1962), 400-424.
IsGreatest {x | ∃ A, ∃ (_ : A.IsIsosceles), A.ncard = x} 8SolvedStatement only, no proof