Erdős problem 212 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

FormalConjectures/ErdosProblems/

212.lean

Retained formal statement1 of 1

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

FormalConjectures/ErdosProblems/212.leanErdos212.erdos_2121 lineExact file

1True ↔ ∃ u, Dense u ∧ u.Pairwise fun c₁ c₂ => dist c₁ c₂ ∈ Set.range Rat.cast

OpenStatement only, no proof