The Falconer distance conjecture in all dimensions

Follow-up works

• Guozheng Cheng, Xiang Fang, Menghan Li, Hongdou Qu, Chengbo Xiao, A quantitative form of the planar Falconer distance theorem (arXiv:2610.22222, 15 October 2026). The abstract says the proof "develops the multiscale method of the September 2026 manuscript of OpenAI" and gives a quantitative lower bound, depending on diameter and Frostman data, for the measure of planar distance sets; the arXiv comments say higher-dimensional cases will follow in later versions.
• Harald Schilly, Erdős similarity for distance sets: finite patterns, a pinned obstruction, and an open window (Zenodo, doi:10.5281/zenodo.23219652, 7 October 2026). States its results conditionally on the all-dimensional Falconer theorem of this paper, together with another OpenAI release result, and reports Lean 4 formalizations; the companion repository says Claude assisted with the repository and paper.

Formalization

• mathcommunity/oai-math-revised, lean/docs/073.md (Lean scope note of the release). States that the formalization covers the strict-threshold compact-set statement in every dimension and the planar case, and links Comparator statements PlanarFalconer.lean and FalconerAllDimensions.lean.
• OpenAI, Campaign123PlanarFurstenbergProof.lean (openai/math, commit adc7f12). Contains falconer_distance_conjecture for all d ≥ 2, derived in Lean via a planar Furstenberg specialization (publishedPlanarFurstenberg_proved), which is also proved in the file.
• OpenAI, FalconerAllDimensions.lean (openai/math Comparator challenge). The target statement for Comparator checking (body sorry by design): compact E ⊂ EuclideanSpace ℝ (Fin d), d/2 < dimH E implies the distance set has positive volume.
• CoolRmal, falconer-all-dimensions (GitHub repository, October 2026). An independent extraction of the release's all-dimensional Lean development with unchanged sources and a provenance manifest; its README reports a passing Comparator run on 6 October 2026 with only the standard three axioms.
• google-deepmind/formal-conjectures, FormalConjectures/Wikipedia/Falconer.lean (formal-conjectures). Independent Lean statements falconer_conjecture (d ≥ 2) and falconer_conjecture_two, stated with sorry, now marked solved and linked to the OpenAI Lean proofs.
• Harald Schilly, math-distance-set-similarity (GitHub repository, 2026). Imports the Falconer theorem as an explicit hypothesis FalconerStatement and, per its README, re-checks that the release's Lean proof discharges it.

Related prior literature mentioned by others

• Shengwen Gan, Bochen Liu, Shukun Wu, Lebesgue measure of distance sets and $L^2$ ball inflation (arXiv:2610.05015, 4 October 2026). Cited in Cheng et al.'s follow-up as prior work giving an alternative pinned planar $5/4$ theorem and positive-measure pinned results under packing-dimension assumptions, without decoupling.
• Nets Hawk Katz and Terence Tao, Some Connections between Falconer's Distance Set Conjecture and Sets of Furstenburg Type (New York Journal of Mathematics 7, 149–187, 2001). Cheng et al.'s follow-up cites its connections among discretized distance, Furstenberg-set and sum-product problems as background for the multiscale approach developed from this paper.

Possibly relevant literature (found by the agent, not checked)

• Marianna Csornyei, D. M. Stull, Hyperplane Incidences and Distance Sets in Higher Dimensions (arXiv:2609.38742, 30 September 2026). Higher-dimensional incidence bounds applied to distance sets of sets with dimension above d/2 in ℝ³ and ℝ⁴; relevant to the paper's higher-dimensional angular/incidence preparation (Sections 3–4).
• Kevin Ren, Hong Wang, Furstenberg sets estimate in the plane (arXiv:2308.08819, 2023). Resolution of the planar Furstenberg set conjecture; the paper's retained incidence input is the Orponen–Shmerkin theorem, and the release's Lean proof passes through a planar Furstenberg specialization.
• Alex Iosevich, Alexia Yavicoli, Improved dimension bounds for Falconer's distance problem in the plane (arXiv:2610.05500, 4 October 2026). Lower bounds for dim_H Δ(E) for planar analytic sets with dim_H E > 1, the same hypothesis range as the d = 2 case of Theorem 1.1.