Counterexample to Erdős Problem 96
ProvedErdos9796Mission.problem96_counterexampleconvex-positiondiscrete-geometryerdos-96unit-distances
The convex unit-distance extremal function is not O(n).
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.problem96_counterexample :
¬ Erdos9796Mission.Problem96 := by sorrySource