AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

The Falconer distance conjecture in all dimensions

Can the mathematical statement in The Falconer distance conjecture in all dimensions be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 073)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'The Falconer distance conjecture in all dimensions'. 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.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 073). The Lean development was not rebuilt locally.