Skip to content

Erdős problem 212

Start work

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

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
True ↔ ∃ u, Dense u ∧ u.Pairwise fun c₁ c₂ => dist c₁ c₂ ∈ Set.range Rat.cast
OpenStatement only, no proof