The Falconer distance conjecture
The Falconer distance conjecture asserts that every compact set E ⊂ ℝd, d ≥ 2, of Hausdorff dimension greater than d/2 determines a set of Euclidean distances {|x − y| : x, y ∈ E} of positive Lebesgue measure. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a proof in every dimension. This page summarizes the published claim and lists publicly available follow-up work.
Background
- According to the manuscript's introduction, Falconer (1985) proved the threshold (d + 1)/2, and his lattice-type examples at dimension d/2 explain the strict inequality. Mattila's spherical-average criterion made Fourier L2 estimates central, and Bourgain connected improvements to restriction phenomena. Later thresholds include Wolff's 4/3 in the plane and Erdoğan's d/2 + 1/3 for d ≥ 3.
- The same introduction lists the decoupling-era results: Du, Guth, Ou, Wang, Wilson and Zhang (9/5 in dimension three), Du and Zhang (d/2 + 1/4 + 1/(8d − 4)), and pinned versions, including Guth, Iosevich, Ou and Wang's planar threshold 5/4.
The original result
- Claim. For every integer d ≥ 2 and every compact E ⊂ ℝd with dimH E > d/2, the distance set has positive Lebesgue measure (Theorem 1.1). The manuscript states that no regularity beyond the strict dimension assumption is required and that no endpoint assertion is made.
- Source. The Falconer distance conjecture in all dimensions in the openai/math repository (commit
1581d4c). - Formalization, as described by the repository. The scope note lean/docs/073.md states that the formalization proves the conjecture in every dimension, and that the linked statements include both the all-dimensional result and the earlier planar case. The Comparator statements are
FalconerAllDimensions.leanandPlanarFalconer.lean. - Catalogue status. Google DeepMind's Formal Conjectures project lists
falconer_conjecture_twoandfalconer_conjecturein FormalConjectures/Wikipedia/Falconer.lean as "research solved", each with aformal_prooflink to the repository's Lean files.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 16 October 2026) |
|---|---|---|---|---|
| 2026-10-06 | CoolRmal/falconer-all-dimensions (GitHub) | Verification run (Comparator) | Isolates the all-dimensional Falconer formalization from the repository with the Lean sources and Comparator challenge unchanged, and records a Comparator run on 6 October 2026 whose log states "Lean default kernel accepts the solution", in a sandbox. | Repository with a saved Comparator log. |
| 2026-10-07 | haraldschilly/math-mattila-sjolin (GitHub) | Use (Lean library) | A Lean 4 proof of the Mattila–Sjölin theorem (a compact set of dimension greater than (d + 1)/2 has a distance set containing an interval) that reuses formal results from OpenAI's Falconer library, such as Frostman's lemma, the Fourier form of the Riesz energy and stationary-phase expansions for sphere decay. | Repository; its README reports only the standard axioms. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates both challenges "full"; records a sandboxed Comparator pass for PlanarFalconer and no machine check for FalconerAllDimensions. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) lists neither Falconer challenge, so both were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-15 (submitted) | G. Cheng, X. Fang, M. Li, H. Qu, C. Xiao, A quantitative form of the planar Falconer distance theorem (arXiv:2610.22222) | Extension (quantitative, planar) | For every 0 < η < 1, a positive lower bound depending only on η for the measure of the distance set of a compact subset of the unit ball supporting a probability measure with ν(B(x, r)) ≤ 2r1+η; the proof "develops the multiscale method of the September 2026 manuscript of OpenAI". The comments say higher dimensions will be addressed in later versions. | arXiv preprint. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.