Wang-Zahl: the three-dimensional Kakeya conjecture

wang_zahl_kakeya_dimH — a formalization challenge from the lean-eval benchmark.

Notes

Every compact subset K of Euclidean three-space that contains a unit line segment in every unit direction has Hausdorff dimension 3. The trusted IsKakeya definition includes compactness, explicitly quantifies over norm-one direction vectors v, and requires a translate of {t • v | 0 ≤ t ≤ 1} to lie in K. Full Hausdorff dimension also forces full lower and upper Minkowski dimension, so this captures both conclusions of Theorem 1.1. Mathlib supplies EuclideanSpace, the normed-space operations, and MeasureTheory.dimH, but not the Kakeya theorem or its tube-estimate machinery.

Formal statement

/-- **Wang--Zahl's three-dimensional Kakeya theorem.** Every Kakeya set in
three-dimensional Euclidean space has full Hausdorff dimension. -/
theorem wang_zahl_kakeya_dimH {K : Set Space} (hK : IsKakeya K) :
    dimH K = 3 := by
  sorry

Informal solution sketch

The upper bound dimH K ≤ 3 is the ambient Euclidean-dimension bound. For the lower bound, discretize the family of unit segments in K at a small scale δ, replacing them by a direction-separated family of δ-tubes. Wang and Zahl establish almost-maximal lower bounds for unions of tubes and their dense shadings under convex non-clustering hypotheses. Starting from Wolff's hairbrush estimate D(1/2, 0), their multi-scale argument combines grains decompositions, refined induction on scales, factorization, and a generalization of the previously established sticky Kakeya theorem to obtain the endpoint tube estimates D(0, 0) and E(0, 0). Applied across scales to the segments in K, these estimates force both the Minkowski and Hausdorff dimensions of K to be at least 3, hence exactly 3.

Source

H. Wang and J. Zahl, 'Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions', Theorem 1.1, arXiv:2502.17655 (2025), https://arxiv.org/abs/2502.17655. The proof builds on their 'Sticky Kakeya sets and the sticky Kakeya conjecture', arXiv:2210.09581, and 'The Assouad dimension of Kakeya sets in R^3', arXiv:2401.12337.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: wang_zahl_kakeya_dimH
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.