Erdős problem 212
Is there a dense subset of ℝ^2 such that all pairwise distances are rational?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/212.leanTrue ↔ ∃ u, Dense u ∧ u.Pairwise fun c₁ c₂ => dist c₁ c₂ ∈ Set.range Rat.castOpenStatement only, no proof