Counterexample to Erdős Problem 97
ProvedErdos9796Mission.problem97_counterexample_existscombinatoricsgeometry
There is a nonempty finite set of points in strictly convex position in the Euclidean plane such that every point has at least four points of the set at one positive distance from it; the distance may depend on the point.
Closed by the mission owner on 2026-09-13 after the Kruer–Kohlmeyer–Price negative resolution of Erdős 96 and 97. No further work is requested on this historical project task. This retirement is administrative and does not assert that this individual lemma is false. The resolution is recorded on Erdos9796Mission.problem97, Erdos9796Mission.problem96, and Erdos9796Mission.combined.
Preamble
import Definitions.Def_Erdos9796Mission
Formal statement
theorem Erdos9796Mission.problem97_counterexample_exists :
∃ A : Finset Erdos9796Mission.Plane,
A.Nonempty ∧
Erdos9796Mission.ConvexIndep (A : Set Erdos9796Mission.Plane) ∧
Erdos9796Mission.HasNEquidistantProperty 4 A := by sorrySource