Skip to content

Erdős problem 97

Start work

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

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.

FormalConjectures/ErdosProblems/97.leanErdos97.erdos_97.variants.three_unit_distance1 lineExact file
∃ A, A.Nonempty ∧ EuclideanGeometry.ConvexIndep ↑A ∧ Erdos97.HasNUnitDistanceProperty 3 A
SolvedStatement only, no proof