# The Falconer distance conjecture

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The Falconer distance conjecture in all dimensions](../../preprints/The-Falconer-distance-conjecture-in-all-dimensions-September-23-2026/paper.pdf)

## Scope

The formalization proves the Falconer distance conjecture in every dimension. For every integer $d\ge2$ and compact set $E\subset\mathbb R^d$ with Hausdorff dimension greater than $d/2$, the set $\{\lVert x-y\rVert:x,y\in E\}$ has positive Lebesgue measure. The linked statements include both this all-dimensional result and the earlier planar case.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Planar Falconer distance theorem | [PlanarFalconer.lean](../ComparatorChallenges/PlanarFalconer.lean) |
| Falconer distance theorem in every dimension | [FalconerAllDimensions.lean](../ComparatorChallenges/FalconerAllDimensions.lean) |