---

Claim. Assuming the continuum hypothesis, for every finite $n$ the space $\mathbb{R}^n$ is the union of countably many sets within each of which all pairwise distances are distinct. So in every model of CH the answer to Problem 1127 is yes in every dimension. In every model where CH fails the answer is no in every dimension, by Davies's Theorem 2: a decomposition of this kind, even of the line, implies CH. The statement is therefore independent of ZFC for each $n$, and so is the statement for all $n$ at once, which is the site's label. This page carries the full claim: Kunen's theorem supplies the positive half in the dimensions $n\ge3$ that Davies's paper left open, and the independence is the two halves together.

Depends on. Davies 1972 for the negative half in every dimension and for both halves in the line and the plane.

Earlier cases. Under CH the line was settled by Erdős and Kakutani in 1943, whose decomposition of $\mathbb{R}$ into countably many rationally independent sets has no repeated distance within a set (on the corpus's source card and their claim page), and the plane by Davies in 1972. Erdős's Scottish Book account [Er81b] poses the question.

Source. Kenneth Kunen, Partitioning Euclidean space, Math. Proc. Cambridge Philos. Soc. 102 (1987), no. 3, 379--383, doi:10.1017/S0305004100067426. The issue is dated November 1987 and carries no day, so this page's date is the first of that month. The paper is not held by this corpus; the publisher's record shows only the opening sentences, and the theorem is recorded as the site's commentary states it. Nothing on this page is independently reviewed by this project.

Acceptance. Refereed: the result is a journal paper in the Mathematical Proceedings of the Cambridge Philosophical Society. Reviewed: the curator of erdosproblems.com, T. F. Bloom, labels Problem 1127 independent and credits Kunen with the case of every $n$ under the continuum hypothesis (problem page last edited 30 December 2025, accessed 2026-10-07). The curator is independent of the author.

Formalization. A Lean proof of the result is the formalization link: the file src/latest/ErdosProblems/Erdos1127.lean in Boris Alexeev's lean-proofs repository, linked at its commit of 2026-09-04. Its header calls it a Lean formalization of a solution to the problem and names Kenneth Kunen as the informal author and Codex and GPT-5.6 Sol as the formal authors. Its theorem erdos_1127 proves that the continuum hypothesis holds if and only if for every finite $n$ there is a coloring of $\mathbb{R}^n$ with countably many colors such that all pairwise distances within a color are distinct, and erdos_1127_real_line proves the same equivalence for the line. So the development proves both halves: Kunen's sufficiency of CH, which the header credits, and the necessity of CH, which is Davies's half (his Theorem 2 strengthens the converse half of Erdős and Kakutani's theorem, which concerns rationally independent sets) and which the header does not name. The file contains no sorry. The corpus has not built the file, so the page lists no formalized evidence.