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

Fishburn and Reeds [FiRe92] also proved that the smallest nn for which there exists a convex nn-gon and a cut {A,B}\{A, B\} of its vertices such that ∣{b∈B:d(a,b)=1}∣≥3|\{b \in B : d(a, b) = 1\}| ≥ 3 for all a∈Aa \in A, and ∣{a∈A:d(a,b)=1}∣≥3|\{a \in A : d(a, b) = 1\}| ≥ 3 for all b∈Bb \in B, is n=20n = 20.

FormalConjectures/ErdosProblems/97.leanErdos97.erdos_97.variants.three_unit_distance_cut_min9 linesExact file
sInf    {n |      ∃ V A B,        n = V.card ∧          EuclideanGeometry.ConvexIndep ↑V ∧            A.Nonempty ∧              B.Nonempty ∧                Erdos97.IsCut V A B ∧ Erdos97.HasNUnitDistancePointsOn 3 B A ∧ Erdos97.HasNUnitDistancePointsOn 3 A B} =  20
SolvedStatement only, no proof