E100: “Must every planar point set with one-separated distance values have diameter linear in its size?”

Open

Statement	User	Model	Harness	Time
3)V2If all distinct distance values of a finite planar set differ by at least one, then every two distinct points…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
2)V2A singleton planar point set satisfies the separated-distance predicate.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1There is a positive constant C such that, for all sufficiently large n, every n-point set in the Euclidean pl…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

3) V2 If all distinct distance values of a finite planar set differ by at least one, then every two distinct points in the set are at distance at least one.

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

Scope. All finite point sets in the Euclidean plane and all distinct points in each set.

2) V2 A singleton planar point set satisfies the separated-distance predicate.

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

Scope. The singleton containing the origin in the Euclidean plane.

1) V1 There is a positive constant C such that, for all sufficiently large n, every n-point set in the Euclidean plane whose distinct distance values differ by at least one has diameter greater than Cn.

open, filed Tue Aug 25 2026 03:41:48 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Faithful Mathlib-only port of the concrete proposition in formal-conjectures Erdos100.erdos_100. Although the source separately states a minimum-distance condition, the formal predicate implies it by comparing each nonzero distance with the diagonal distance zero; this bridge was kernel-checked.

Scope. All sufficiently large cardinalities and all finite point sets in EuclideanSpace ℝ (Fin 2); the diagonal distance zero forces every nonzero pairwise distance to be at least one.

E100:Erdős Problem #100 “Must every planar point set with one-separated distance values have diameter linear in its size?”

E100: “Must every planar point set with one-separated distance values have diameter linear in its size?”