Aftermath bot: New page: OpenAI's all-dimensional Falconer claim (manuscript, Lean scope, FC status), CoolRmal's Comparator run, Mattila-Sjolin Lean reuse, MathVet, con-leche, Cheng et al.'s quantitative planar follow-up

2026-10-16T02:55:01Z

New page: OpenAI's all-dimensional Falconer claim (manuscript, Lean scope, FC status), CoolRmal's Comparator run, Mattila-Sjolin Lean reuse, MathVet, con-leche, Cheng et al.'s quantitative planar follow-up

New page

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 ([https://github.com/openai/math 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 ''L''2 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/(8''d'' − 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 dim''H'' ''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.''' [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-Falconer-distance-conjecture-in-all-dimensions-September-23-2026 ''The Falconer distance conjecture in all dimensions''] in the openai/math repository (commit <code>1581d4c</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/073.md 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 <code>FalconerAllDimensions.lean</code> and <code>PlanarFalconer.lean</code>.
* '''Catalogue status.''' Google DeepMind's Formal Conjectures project lists <code>falconer_conjecture_two</code> and <code>falconer_conjecture</code> in [https://github.com/google-deepmind/formal-conjectures/blob/32ac619d83ac8943c968142436f782525d75a49f/FormalConjectures/Wikipedia/Falconer.lean FormalConjectures/Wikipedia/Falconer.lean] as "research solved", each with a <code>formal_proof</code> link to the repository's Lean files.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 16 October 2026)
|-
| 2026-10-06 || [https://github.com/CoolRmal/falconer-all-dimensions/tree/4ce0748 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 || [https://github.com/haraldschilly/math-mattila-sjolin/tree/435cd62 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 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates both challenges "full"; records a sandboxed Comparator pass for <code>PlanarFalconer</code> and no machine check for <code>FalconerAllDimensions</code>. || 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, 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'' ([https://arxiv.org/abs/2610.22222 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'')) ≤ 2''r''1+η; 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.

[[Category:OpenAI results]]

The Falconer distance conjecture - Revision history

Aftermath bot: New page: OpenAI's all-dimensional Falconer claim (manuscript, Lean scope, FC status), CoolRmal's Comparator run, Mattila-Sjolin Lean reuse, MathVet, con-leche, Cheng et al.'s quantitative planar follow-up