---
id: "2026-10-06-openai-falconer-distance-conjecture-lean"
url: "https://postcutoff.com/e/2026-10-06-openai-falconer-distance-conjecture-lean/"
as_of: "2026-10-30T13:42:00+01:00"
date: "2026-10-06"
date_precision: day
category: science
importance: 4
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 6
editor: human editor
human_review: null
version: "2026-10-29"
---

As of: 2026-10-30 13:42 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-06-openai-falconer-distance-conjecture-lean/

# OpenAI proves the Falconer distance conjecture (Lean)

Full title: OpenAI's release proves Falconer's distance conjecture (1985) in every dimension, with a Lean proof of the exact statement

"The Falconer distance conjecture in all dimensions" (OpenAI, 23 Sep 2026, family 073 of the 6 Oct release) proves: "For every integer d ≥ 2, a compact subset of ℝᵈ with Hausdorff dimension greater than d/2 determines a set of Euclidean distances of positive Lebesgue measure." Falconer had shown (d+1)/2 suffices; the best planar bound was 5/4 (Guth–Iosevich–Ou–Wang, 2020), and higher-dimensional bounds stayed above d/2 + 1/4 − 1/(8d+4). The manuscript uses a multiscale analysis of measures with radial projection and incidence inputs. The all-dimensional statement and the planar case are formalized in Lean and accepted by the comparator. No expert assessment has been published; a quantitative planar version by Cheng, Fang, Li, Qu and Xiao develops the method.

## Key facts
- Abstract (verbatim): 'We resolve the Falconer distance conjecture in every dimension. For every integer d ≥ 2, a compact subset of ℝᵈ with Hausdorff dimension greater than d/2 determines a set of Euclidean distances of positive Lebesgue measure.' 64 pages, dated 23 Sep 2026
- Prior state (paper, §1.1): Falconer's threshold (d+1)/2; Wolff's planar 4/3; Erdoğan's d/2 + 1/3 for d ≥ 3; Du, Guth, Ou, Wang, Wilson and Zhang 9/5 in dimension three; Du–Zhang d/2 + 1/4 + 1/(8d − 4); Guth, Iosevich, Ou and Wang dimH E > 5/4 in the plane; Du, Ou, Ren and Zhang d/2 + 1/4 − 1/(8d + 4) for d ≥ 3. Shmerkin and Wang handled sets whose Hausdorff and packing dimensions both equal d/2
- Method (paper, §1.2): a multiscale decomposition of measures into regular pieces with scale-dependent angular tests, building on Keleti–Shmerkin, Shmerkin–Wang and Orponen–Shmerkin; the retained incidence input is the Orponen–Shmerkin theorem; a 'two-depth potential' pays the costs of the recursion
- Lean: comparator challenge FalconerAllDimensions.lean, theorem `falconer_distance_conjecture`: for every d ≥ 2 and compact E ⊆ EuclideanSpace ℝ (Fin d) with d/2 < dimH E, `0 < volume {r : ℝ | ∃ x ∈ E, ∃ y ∈ E, dist x y = r}`; plus PlanarFalconer.lean for the earlier planar case. Only Mathlib definitions are used, so the statement reads as the standard conjecture (our reading). Both were accepted in the oai-math-revised comparator run (25–26 Oct)
- Follow-up: Guozheng Cheng, Xiang Fang, Menghan Li, Hongdou Qu and Chengbo Xiao, 'A quantitative form of the planar Falconer distance theorem' (arXiv 2610.22222, 15 Oct): 'The proof develops the multiscale method of the September 2026 manuscript of OpenAI'; their comment line promises higher dimensions 'building on the October 6 release of the OpenAI preprint'. Their AI note: an AI tool was used for language editing, LaTeX and 'local mathematical reasoning'
- Our 19 Oct entry on the harmonic-analysis claims noted that 073 is among the few families in that area with a Lean link (see [2026-10-06-openai-release-3d-restriction-bochner-riesz-claims](https://postcutoff.com/e/2026-10-06-openai-release-3d-restriction-bochner-riesz-claims/index.md)); no press article or expert blog post on this family was found by 29 Oct

## What happened

How big must a set be before the distances between its points fill out an interval of positive length? Kenneth Falconer showed in
1985 that Hausdorff dimension above (d+1)/2 is enough in ℝᵈ, and conjectured that d/2 suffices, which would be sharp. The problem
is a continuous cousin of Erdős's distinct-distances problem and became a test case for Fourier restriction and decoupling. Progress
was slow: the planar threshold went from 4/3 (Wolff, 1999) to 5/4 (Guth, Iosevich, Ou and Wang, 2020).

OpenAI's 64-page manuscript claims the full conjecture in every dimension. It works directly with the distance measure through a
multiscale decomposition of the set's measure, angular tests at each scale and a recursive potential argument, using known
incidence and radial projection theorems as inputs. The main theorem is formalized in Lean against a statement written with
Mathlib's Hausdorff dimension and Lebesgue measure, and the comparator check passed.

## Why it matters

Falconer's conjecture is one of the central problems linking geometric measure theory and harmonic analysis. With a Lean proof of a
faithful statement it is among the better-checked claims in the release, but human understanding of the argument is only beginning.

## What is disputed or not yet verified

- Verification: Lean formalization of the main theorem; no published human verification yet

## Reactions

The first outside paper, by Guozheng Cheng, Xiang Fang, Menghan Li, Hongdou Qu and Chengbo Xiao, gives a quantitative planar version
by developing the manuscript's multiscale method and promises the higher-dimensional case. We found no blog post, talk or press piece assessing the proof.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 189 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 128 days after its cutoff

## Sources

1. [OpenAI: The Falconer distance conjecture in all dimensions (23 Sep)](https://github.com/openai/math/blob/main/preprints/The-Falconer-distance-conjecture-in-all-dimensions-September-23-2026/paper.pdf) (github.com, paper)
2. [Lean scope note for family 073](https://github.com/openai/math/blob/main/lean/docs/073.md) (github.com, code)
3. [Lean comparator challenge: FalconerAllDimensions.lean](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/FalconerAllDimensions.lean) (github.com, code)
4. [arXiv 2610.22222: Cheng, Fang, Li, Qu, Xiao, A quantitative form of the planar Falconer distance theorem](https://arxiv.org/abs/2610.22222) (arxiv.org, paper)
5. [oai-math-revised: comparator run on all challenges (LEAN_CHECKS.md)](https://github.com/mathcommunity/oai-math-revised/blob/main/docs/LEAN_CHECKS.md) (github.com, code)
6. [oai-math-revised: community notes on the Falconer manuscript](https://github.com/mathcommunity/oai-math-revised/blob/main/preprints/The-Falconer-distance-conjecture-in-all-dimensions-September-23-2026/AGENT_NOTES.md) (github.com, discussion)

## Changes

- 2026-10-29 (filed): Created (families 001–125; manuscript introduction, Lean statement, comparator results and the follow-up arXiv paper read)

## Related

- 2026-10-16: [arXiv results with disclosed AI help, 15 Oct 2026 listing](https://postcutoff.com/e/2026-10-16-ai-assisted-results-october-15-listing/index.md)
- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-10-06: [OpenAI claims 3D restriction and Bochner–Riesz conjectures](https://postcutoff.com/e/2026-10-06-openai-release-3d-restriction-bochner-riesz-claims/index.md)