Erdős Problem 212

Reference: erdosproblems.com/212

theorem Erdos212.erdos_212 : (∃ (u : Set ℂ), Dense u ∧ u.Pairwise fun (c₁ c₂ : ℂ) => dist c₁ c₂ ∈ Set.range Rat.cast) ↔ sorry

Is there a dense subset of ℝ^2 such that all pairwise distances are rational?