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 statement3 of 5

Erdős originally conjectured this (in [Er46b]) with no 3 vertices equidistant, but Danzer found a convex polygon on 9 points such that every vertex has three vertices equidistant from it (but this distance depends on the vertex). Danzer's construction is explained in [Er87b].

[Er46b] Erdős, P., _On sets of distances of $n$ points_. Amer. Math. Monthly (1946), 248-250. [Er87b] Erdős, P., _Some combinatorial and metric problems in geometry_. Intuitive geometry (Siófok, 1985), 167-177.

FormalConjectures/ErdosProblems/97.leanErdos97.erdos_97.variants.three_equidistant1 lineExact file

1∃ A, A.Nonempty ∧ EuclideanGeometry.ConvexIndep ↑A ∧ Erdos97.HasNEquidistantProperty 3 A

SolvedStatement only, no proof

Sources

Search problems.science