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

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

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

1sInf2    {n |3      ∃ V A B,4        n = V.card ∧5          EuclideanGeometry.ConvexIndep ↑V ∧6            A.Nonempty ∧7              B.Nonempty ∧8                Erdos97.IsCut V A B ∧ Erdos97.HasNUnitDistancePointsOn 3 B A ∧ Erdos97.HasNUnitDistancePointsOn 3 A B} =9  20

SolvedStatement only, no proof

Sources

Search problems.science