Problem 97 and its pinned multiplicity formulation
ProvedErdos9796Mission.problem97_iff_exists_pinnedMultiplicity_le_threediscrete-geometryerdos-97pinned-distancesreformulation
Problem 97 implies that every nonempty finite planar point set in strictly convex position contains a point whose pinned distance multiplicity is at most three. The converse implication also holds. These two implications restate the open problem without proving it.
Preamble
import Definitions.Def_Erdos9796Mission_PinnedMultiplicity
Formal statement
theorem Erdos9796Mission.problem97_iff_exists_pinnedMultiplicity_le_three :
Erdos9796Mission.Problem97 ↔
∀ A : Finset Erdos9796Mission.Plane,
A.Nonempty → Erdos9796Mission.ConvexIndep (A : Set Erdos9796Mission.Plane) →
∃ p ∈ A, Erdos9796Mission.pinnedMultiplicity A p ≤ 3 := by sorrySource