Erdős Problem 97: a vertex without four equidistant neighbours
DisprovedErdos9796Mission.problem97For every nonempty finite set of points in strictly convex position in the Euclidean plane, there is a vertex such that every circle of positive radius centred at contains at most three points of .
The set is finite and convex-independent: each vertex lies outside the convex hull of all the others. No lower bound of three on the cardinality is imposed; singletons and two-point sets are included. This is the affirmative target of Problem 97, which remains open in the repository.
import Definitions.Def_Erdos9796Mission /-! The open Erdős Problem 97 statement in the self-contained mission vocabulary. -/
theorem Erdos9796Mission.problem97 : Erdos9796Mission.Problem97 := by sorry
Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
The declaration asserts that for every finite point set in the Euclidean plane, if is nonempty and every point of is absent from the convex hull over of the remaining points , then there is at least one point for which no positive real radius has at least four points at distance exactly from . In expanded form, for that point , every satisfies . The theorem body is sorry, so this is an asserted target rather than an established result.
Confirmed by the mission captain (proposal self-audit).