Erdős problem 97
Does every convex polygon have a vertex with no other 4 vertices equidistant from it?
Sources
FormalConjectures/ErdosProblems/
97.lean
Retained formal statement
Fishburn and Reeds [FiRe92] have found a convex polygon on 20 points such that every vertex has three vertices equidistant from it (and this distance is the same for all vertices).
[FiRe92] Fishburn, P. C. and Reeds, J. A., _Unit distances between vertices of a convex polygon_. Comput. Geom. (1992), 81-91.
∃ A, A.Nonempty ∧ EuclideanGeometry.ConvexIndep ↑A ∧ Erdos97.HasNUnitDistanceProperty 3 ASolvedStatement only, no proof