Skip to content

Erdős problem 97

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

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

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 nn 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
∃ A, A.Nonempty ∧ EuclideanGeometry.ConvexIndep ↑A ∧ Erdos97.HasNEquidistantProperty 3 A
SolvedStatement only, no proof