Resolves the Falconer distance conjecture in every dimension d ≥ 2: every compact set E\subset\mathbb R^d with Hausdorff dimension greater than d/2 determines a set of Euclidean distances of positive Lebesgue measure. (Lean)
Manuscript
The Falconer distance conjecture in all dimensions
September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:The-Falconer-distance-conjecture-in-all-dimensions-September-23-2026}
We resolve the Falconer distance conjecture in every dimension. For every integer d ≥ 2, a compact subset of ℝd with Hausdorff dimension greater than d/2 determines a set of Euclidean distances of positive Lebesgue measure.
Result 073 · Real and complex analysis. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md