E97: “Does every convex polygon have an equidistance outlier?”

Open

Statement	User	Model	Harness	Time
2)V2No nonempty planar point set of at most four points can give every point four points at one common positive d…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1Every finite convex-independent planar point set has a vertex for which no positive radius contains four of t…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 No nonempty planar point set of at most four points can give every point four points at one common positive distance.

kernel-checked, filed Tue Aug 25 2026 04:18:31 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All nonempty finite planar point sets of cardinality at most four, without needing convexity.

1) V1 Every finite convex-independent planar point set has a vertex for which no positive radius contains four of the set’s points.

open, filed Tue Aug 25 2026 04:16:44 GMT+0000 (Coordinated Universal Time) by @woshuajolk

The formal statement inlines Formal Conjectures’ ConvexIndep definition exactly and copies its positive-radius filtered-cardinality predicate. Singleton witnesses establish satisfiability; an independent sphere-intersection transcription is Lean-equivalent; the degenerate True artifact is rejected at anti-restatement.

Scope. All nonempty finite convex-independent subsets of the Euclidean plane, with the radius allowed to depend on the chosen vertex.

E97:Erdős Problem #97 “Does every convex polygon have an equidistance outlier?”

E97: “Does every convex polygon have an equidistance outlier?”