Every n points in the plane contain (m1 + o(1)) n points with no unit distance
Abstract
Let f(n) be the largest integer such that every set of n points in the plane contains f(n) points no two at distance $1$, and let m1 be the supremum of the upper densities of Lebesgue measurable planar sets with no two points at distance $1$. Larman and Rogers observed that f(n) ≥ m1 n. We prove that f(n)/n → m1; that is, f(n) = (m1 + o(1))n. This is the first half of a conjecture of Dúcz and Varga, and with the bound m1 ≤ 0.247 of Ambrus, Csiszárik, Matolcsi, Varga and Zsámboki it gives f(n) ≤ (0.247 + o(1))n. The proof builds a random independent subset of the algebraic plane, invariant under algebraic translations and rotations, whose probability of containing the origin is at least the worst finite independence ratio, and turns it into a measurable planar set of at least that upper density. Its only non-classical input is the Haar rigidity theorem for wild character laws from the OpenAI preprint The Euclidean plane is not five-colorable, which has a machine-checked Lean proof. The whole argument has been formalized in Lean 4 on top of it.
Related
- A Moser-spindle-free 5-chromatic unit distance graph on 2131 vertices in the plane
- Algorithmic exploration of the unit distance problem in the rational plane
- Large Planar Point Sets Contain 4 Collinear Points or Almost 7-Cliques, and Related Results
- A 21-Coloring of the Plane Without Monochromatic Unit-Area Rectangles
- An explicit lower bound for the unit distance problem
BibTeX
@misc{li2026every,
title = {{Every n points in the plane contain (m1 + o(1)) n points with no unit distance}},
author = {Shisheng Li and Yong Su},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.15424},
eprint = {2610.15424},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.15424},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Every n points in the plane contain (m1 + o(1)) n points with no unit distance
AU - Shisheng Li
AU - Yong Su
PY - 2026
DA - 2026/10/11
PB - arXiv
DO - 10.48550/arxiv.2610.15424
UR - https://arxiv.org/abs/2610.15424
AB - Let f(n) be the largest integer such that every set of n points in the plane contains f(n) points no two at distance $1$, and let m_1 be the supremum of the upper densities of Lebesgue measurable planar sets with no two points at distance $1$. Larman and Rogers observed that f(n) ≥ m_1 n. We prove that f(n)/n → m_1; that is, f(n) = (m_1 + o(1))n. This is the first half of a conjecture of Dúcz and Varga, and with the bound m_1 ≤ 0.247 of Ambrus, Csiszárik, Matolcsi, Varga and Zsámboki it gives f(n) ≤ (0.247 + o(1))n. The proof builds a random independent subset of the algebraic plane, invariant under algebraic translations and rotations, whose probability of containing the origin is at least the worst finite independence ratio, and turns it into a measurable planar set of at least that upper density. Its only non-classical input is the Haar rigidity theorem for wild character laws from the OpenAI preprint The Euclidean plane is not five-colorable, which has a machine-checked Lean proof. The whole argument has been formalized in Lean 4 on top of it.
ER -