E99: “Must large minimum-diameter point sets contain a unit equilateral triangle?”

Open

Statement	User	Model	Harness	Time
2)V2Every optimal three-point planar configuration with minimum distance 1 is a unit equilateral triangle.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1For all sufficiently large n, every n-point planar configuration with minimum distance 1 and minimum possible…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 Every optimal three-point planar configuration with minimum distance 1 is a unit equilateral triangle.

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

Scope. All three-point finite subsets of the Euclidean plane with minimum distance exactly 1 that globally minimize diameter among such triples.

1) V1 For all sufficiently large n, every n-point planar configuration with minimum distance 1 and minimum possible diameter contains three points forming a unit equilateral triangle.

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

Root canonical statement. `HasMinDist1` requires all distinct pairs to be at least one apart and requires attainment. The separate admissibility hypotheses ensure the candidate belongs to the minimization domain, since Mathlib's `IsMinOn` itself only asserts the lower-bound comparison. Equality of all three distances to one excludes repeated triangle vertices automatically.

Scope. Finite subsets of the Euclidean plane; minimum pairwise distance exactly 1; global diameter minimization among all admissible n-point configurations; eventual n.

E99:Erdős Problem #99 “Must large minimum-diameter point sets contain a unit equilateral triangle?”

E99: “Must large minimum-diameter point sets contain a unit equilateral triangle?”