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 6 (due to Kelly [ErKe47] - an alternative proof is given by Kovács [Ko24c]).
[ErKe47] Erdős, Paul and Kelly, L. M., Elementary Problems and Solutions: Solutions: E735. Amer. Math. Monthly (1947), 227-229. [Ko24c] Z. Kovács, A note on Erdős's mysterious remark. arXiv:2412.05190 (2024).
IsGreatest {x | ∃ A, ∃ (_ : A.IsIsosceles), A.ncard = x} 6SolvedStatement only, no proof