Every n points in the plane contain (m1 + o(1)) n points with no unit distance
Shisheng Li, Yong Su
math.CO
Oct 11, 2026 · v1
math.MG
TL;DR
The full proof that f(n)/n tends to m1 is formalized in Lean 4 with Mathlib, building on OpenAI's Lean development of the plane five-colouring Haar rigidity theorem.
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 $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) \ge m_1 n$. We prove that $f(n)/n \to 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 \le 0.247$ of Ambrus, Csiszárik, Matolcsi, Varga and Zsámboki it gives $f(n) \le (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.
Problem
Let f(n) be the largest number such that every n-point planar set contains f(n) points with no two at unit distance, and let m1 be the supremum of upper densities of measurable unit-distance-free planar sets. Larman and Rogers showed f(n) ≥ m1 n. Dúcz and Varga conjectured that f(n)/n → m1.
Approach
The authors show that f(n)/n converges to the worst finite independence ratio α*, and recall that α* ≥ m1. For the new direction, m1 ≥ α*, they build a random independent subset of the algebraic plane, invariant under algebraic translations and rotations, and transfer it to a measurable planar set. This step uses the Haar rigidity theorem for wild character laws from OpenAI's five-colorability preprint. The argument is formalized in Lean 4 on top of OpenAI's Lean development, using ultrafilter limits and the Riesz–Markov theorem.
Results
They prove that f(n)/n → m1 and that f(n) ≥ m1 n for all n. Combined with known bounds, this gives 0.22936n ≤ f(n) ≤ (0.247+o(1))n. The Lean proofs cover the square (natural radius) and disc (real radius) density conventions and depend only on the standard axioms.
