Convex and discrete geometry
Erdős 212
Is there a dense subset of ℝ^2 such that all pairwise distances are rational?References
No one has attempted this yet.
Formal statement
Lean type
True ↔ ∃ u, Dense u ∧ u.Pairwise fun c₁ c₂ => dist c₁ c₂ ∈ Set.range Rat.castWhat you must prove
import FormalConjectures.ErdosProblems.«212»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos212.erdos_212" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/212.lean
- Source type SHA-256
- sha256:a946ed3b4bc15a6ec18803c08ebd1d8f4a9362eaa079a85bccc95526ce01fc22
- Task id
- fc-379fc029-erdos212-erdos-212-9186d1d2e0-formalized-v1
- Task commitment
- sha256:b014a6420e2629e462631561f84a2b0518cdf085742161295f4df8f781d61ef6
Something wrong with this formalization?
A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.