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
Does every convex polygon have a vertex with no other 4 vertices equidistant from it?
True ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.Nonempty → EuclideanGeometry.ConvexIndep ↑A → ¬Erdos97.HasNEquidistantProperty 4 AOpenStatement only, no proof