Erdős–Ulam problem: is there a dense subset of the plane with all pairwise distances rational? (Erdős #212)
Statement
Is there a subset of $\mathbb{R}^2$, topologically dense in the plane, such that all pairwise distances between its points are rational?
Acceptance. FULLY RESOLVES: an UNCONDITIONAL proof that no dense subset of $\mathbb{R}^2$ has all pairwise distances rational (a proof conditional on Bombieri–Lang does not qualify — that is already known, per Tao and Shaffaf); or, in the other direction, an explicit construction of a dense rational-distance set with complete proofs of density and of the rationality of all pairwise distances. Machine-checkable (Lean/Coq) proof preferred, else a complete written proof. ADVANCES: (a) an unconditional proof that a rational-distance set cannot be dense in the plane under any weakened hypothesis (e.g. assuming general position, or for sets dense in some open set); (b) an unconditional strengthening of the Solymosi–de Zeeuw curve theorem, e.g. quantitative bounds on rational-distance points on curves of given degree strictly beyond what is stated in the background; (c) a proof or disproof of Besicovitch's conjecture on the limit points of rational-distance sets; (d) a machine-checked (Lean) formalisation of the Solymosi–de Zeeuw theorem or of the Tao/Shaffaf conditional argument. Deliver the proof file (or formalisation repository) as the artifact.
Background
Conjectured (in the negative) by Ulam, and a favourite of Erdős, appearing in [Er61, p.246], [Er75f, p.107], [Er83c] and [Er87b, p.172]; listed as open on erdosproblems.com/212 (fetched 2026-07-13, status 'open', tagged 'geometry | distances'). Erdős believed no such set exists. The modern frontier is conditional: Terence Tao showed in a 2014 blogpost that the Bombieri–Lang conjecture implies there is no dense rational-distance set, and the same conclusion was obtained independently by Shaffaf [Sh18] — indeed both show a rational-distance set that is dense (even Zariski-dense enough) must be contained in a finite union of real algebraic curves. Unconditionally, Solymosi and de Zeeuw [SdZ10] proved that a rational-distance set contained in a real algebraic curve is finite unless the curve contains a line or a circle — the exception is necessary, since the rational points of a line, and classical constructions on circles, give dense rational-distance subsets of those curves. Ascher, Braune and Turchet [ABT20] observed that combining these results shows (still conditional on Bombieri–Lang) that a rational-distance set in general position — no three points collinear, no four concyclic — must be finite. Erdős [Er87b] also records Besicovitch's conjecture that the set of limit points of a rational-distance set cannot contain arbitrarily large convex sets. Note that a conditional resolution is already known, so the open problem is the UNCONDITIONAL one. The statement is formalised in Lean in DeepMind's formal-conjectures repository. The attacker's tools: arithmetic geometry — establishing the needed cases of Bombieri–Lang for the specific surfaces that arise, or new unconditional finiteness arguments; or machine-checked formalisation of the unconditional Solymosi–de Zeeuw theorem.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #212 (T. F. Bloom) | website |
| REF-02 | T. Tao — The Erdős–Ulam problem, varieties of general type, and the Bombieri–Lang conjecture | website |
| REF-03 | Formalised Lean statement of Erdős #212 (google-deepmind/formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.