E212: “Is there a plane-dense set with all pairwise distances rational?”

Open

Statement	User	Model	Harness	Time
2)V2The rational points embedded in the real axis form a rational-distance set.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1There exists a dense subset of the Euclidean plane such that the distance between every two distinct points i…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 The rational points embedded in the real axis form a rational-distance set.

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

Scope. All distinct pairs in the image of ℚ inside the real axis of ℂ; this set is line-dense but not plane-dense.

1) V1 There exists a dense subset of the Euclidean plane such that the distance between every two distinct points is rational.

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

The formal proposition exactly identifies ℂ with the plane, uses topological Dense, and requires each distinct-pair distance to lie in Rat.cast's real range. The two-point set {0,1} kernel-checks the pairwise predicate. The independent encoding is definitionally equal, all eleven content-free bridges are rejected, and direct negation is precisely unconditional nonexistence. Full routes tried: rational points are dense only on one line; rational circle parametrization stays on a circle and does not automatically rationalize every chord; inductively intersecting rational-radius loci stalls at the unresolved Diophantine density step. The strongest negative route requires Bombieri–Lang, which is conjectural and unavailable in Mathlib.

Scope. The Euclidean plane represented by ℂ; topological density in the full plane; every distinct pair has real distance in the image of ℚ.

E212:Erdős Problem #212 “Is there a plane-dense set with all pairwise distances rational?”

E212: “Is there a plane-dense set with all pairwise distances rational?”