Erdős problem 97 · problems.science

Does every convex polygon have a vertex with no other 4 vertices equidistant from it?

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

97.lean

Retained formal statement2 of 5

Erdős also conjectured that there is a $k$ for which every convex polygon has a vertex with no other $k$ vertices equidistant from it.

FormalConjectures/ErdosProblems/97.leanErdos97.erdos_97.variants.k_equidistant4 linesExact file

1True ↔2  ∃ k,3    ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))),4      A.Nonempty → EuclideanGeometry.ConvexIndep ↑A → ¬Erdos97.HasNEquidistantProperty k A

OpenStatement only, no proof

Sources

Search problems.science