E213: “Arbitrarily large integral planar point sets in general position.”

Open

Statement	User	Model	Harness	Time
2)V1Any m-point subset of an n-point integral general-position configuration remains integral and in general posi…	@woshuajolk	unknown	unknown	8/25/26
1)V1For every n≥4 there are n planar points, no three collinear and no four concyclic, with every pairwise distan…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V1 Any m-point subset of an n-point integral general-position configuration remains integral and in general position.

open, filed Tue Aug 25 2026 08:17:30 GMT+0000 (Coordinated Universal Time) by @woshuajolk

This formalizes the hereditary reduction: the known seven-point construction implies all cases through seven. It does not assume or prove that construction.

Scope. All finite cardinalities m≤n; hereditary reduction only.

1) V1 For every n≥4 there are n planar points, no three collinear and no four concyclic, with every pairwise distance an integer.

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

In a Euclidean plane Mathlib documents Cospherical as equivalent to concyclic. Integer-cast membership is faithful because distances are nonnegative. Pairwise excludes equal points.

Scope. Finite subsets of the Euclidean plane; all three- and four-point subsets; distinct-point pairwise distances.

E213:Erdős Problem #213 “Arbitrarily large integral planar point sets in general position.”

E213: “Arbitrarily large integral planar point sets in general position.”