Lean-Eval problem wang_zahl_kakeya_dimH (submitted by Kim Morrison). 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.Lean-Eval 题目 wang_zahl_kakeya_dimH（提交者 Kim Morrison）。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. github.com/leanprover/lean-eval
When LOT proved this problem, a 3-level chain of intermediate theorems closed at once: each level is proved from the one below. We checked that chain twice, at the same time on two identical 20-CPU / 64 GiB workers: once with Lean’s original pipeline and once with LOT’s infrastructure, all six optimizations on. Both runs accepted every level.LOT 证这道题时，有一条 3 层的中间定理链同时收口：每一层都由下一层推出。我们把这条链检查了两遍，两遍同时运行，分别在两台相同的 20 核 / 64 GiB worker 上：一遍用 Lean 原始流程，一遍用 LOT 基础设施（6 项优化全开）。两遍都接受了每一层。
Premise. Both runs start from the same situation: every theorem of the chain is already proved. LOT’s run also assumes what LOT has already done by then: the levels below were pre-checked, so their build artefacts (and the ledger they taught) are ready to reuse. That earlier work happens while the agents are still proving; its cost is not inside the LOT time below and is reported separately on this page as it is measured.前提。两遍检查从相同的情况开始：链上每个定理都已经证明完毕。LOT 那一遍还默认 LOT 此前已经做完的工作：下面各层已经做过预检查，它们的编译产物（以及账本学到的结果）可以直接复用。这部分工作发生在 agent 还在证明的时候，不计入下面 LOT 的用时，测出来后在本页单独列出。
What the two times are. Lean original is the wall-clock time to check the 3 levels one after another on one worker, each from scratch with the unmodified official checker. LOT’s infrastructure (all six optimizations on) is the wall-clock time of the latest pipeline on the same chain: a probe build that reuses the artefacts of the level below, then one check of the whole chain with parallel kernel replay. In this single replay the ledger is on but starts empty, and the queueing and speculative-checking optimizations, which act across a whole tree, have nothing to overlap with. Neither time includes the root check, queue waits or the scheduler’s pauses. The chain is not necessarily the tree’s longest: it is one closing cascade, the levels that became checkable one after another when the bottom theorem was proved, chosen for size and variety.两个时间分别是什么。Lean 原始流程：在一台 worker 上把这 3 层依次检查完的总用时，每层都用未改动的官方检查器从头检查。LOT 基础设施（6 项优化全开）：最新流程检查同一条链的总用时，先做一次复用下一层编译产物的探测编译，再用并行内核重放把整条链一次查完。在这次单独回放里，账本虽然开着但从空开始；排队和推测并行检查这两项是在整棵树的层面起作用的，这里没有可以重叠的东西。两个时间都不含根检查、排队等待和调度器的停顿。这条链不一定是这棵树里最长的：它是一次“收口”，即最底层定理证完后，上面各层依次变得可检查；挑选时兼顾规模和多样性。
Each bar spans its own run from start to finish, drawn from the measured stage times, so both end at the same length; the minutes on the right and the shared clock show how long each run really took. White ticks separate the levels.每条色条从头到尾对应各自那次运行，按实测各阶段用时画出，所以两条最终一样长；右侧分钟数和共用的时钟显示各自的真实用时。白色刻线分隔各层。
A level lights up when a run has checked it: red for the original pipeline, teal for the optimized one.某次运行检查完一层，该层就会亮起：红色是原始流程，青色是优化后的流程。
wz_dense_transverse_brush_boundA given subfamily of rho-dense tubes meeting one stem at projective angle at least b and satisfying convex count m has union volume at least c_(epsilon,b)*delta^(2+epsilon)*rho^3*m^-1*card(F).
∀ ε b : ℝ, 0 < ε → 0 < b → b ≤ 1 → ∃ d : ℝ, 0 < d ∧ ∀ δ rho m : ℝ, 0 < δ → δ ≤ (1 / 100 : ℝ) → 0 < rho → rho ≤ 1 → 1 ≤ m → ∀ (n : ℕ) (x v : Fin n → LeanEval.Analysis.WangZahlKakeya.Space) (Y : Fin n → Set LeanEval.Analysis.WangZahlKakeya.Space), (∀ i : Fin n, ‖v i‖ = 1) → (∀ i : Fin n, Metric.thickening δ (segment ℝ (x i) (x i + v i)) ⊆ Metric.ball (0 : LeanEval.Analysis.WangZahlKakeya.Space) 1) → (∀ i : Fin n, MeasurableSet (Y i)) → (∀ i : Fin n, Y i ⊆ Metric.thickening δ (segment ℝ (x i) (x i + v i))) → (∀ W : Set LeanEval.Analysis.WangZahlKakeya.Space, Convex ℝ W → ENNReal.ofReal (((Set.ncard {i : Fin n | Metric.thickening δ (segment ℝ (x i) (x i + v i)) ⊆ W} : ℕ) : ℝ) * δ ^ 2) ≤ ENNReal.ofReal m * MeasureTheory.volume W) → ∀ (i₀ : Fin n) (F : Finset (Fin n)), (∀ i : Fin n, i ∈ F → (Metric.thickening δ (segment ℝ (x i) (x i + v i)) ∩ Metric.thickening δ (segment ℝ (x i₀) (x i₀ + v i₀))).Nonempty) → (∀ i : Fin n, i ∈ F → b ≤ min ‖v i - v i₀‖ ‖v i + v i₀‖) → (∀ i : Fin n, i ∈ F → ENNReal.ofReal (rho * δ ^ 2) ≤ MeasureTheory.volume (Y i)) → d * δ ^ ((2 : ℝ) + ε) * rho ^ 3 * m⁻¹ * (F.card : ℝ) ≤ (MeasureTheory.volume (⋃ i : Fin n, Y i)).toRealwz_broad_hairbrush_boundA universal polynomial-loss Wolff hairbrush bound for half-cap broad shadings: there exists K >= 1, independent of the aperture and epsilon, such that average density lam and convex count m imply union volume at least c * delta^(3/2+epsilon) * lam^K * m^(-K) * sqrt(n). Half-cap broadness is the explicit pointwise projective-cap count in the frozen type. No slab or essential-distinctness hypothesis is required.
∃ K : ℝ, 1 ≤ K ∧ ∀ α b : ℝ, 0 < α → 0 < b → b ≤ 1 → ∃ c : ℝ, 0 < c ∧ ∀ δ lam m : ℝ, 0 < δ → δ ≤ (1 / 100 : ℝ) → 0 < lam → lam ≤ 1 → 1 ≤ m → ∀ (n : ℕ) (x v : Fin n → LeanEval.Analysis.WangZahlKakeya.Space) (Y : Fin n → Set LeanEval.Analysis.WangZahlKakeya.Space), 0 < n → (∀ i : Fin n, ‖v i‖ = 1) → (∀ i : Fin n, Metric.thickening δ (segment ℝ (x i) (x i + v i)) ⊆ Metric.ball (0 : LeanEval.Analysis.WangZahlKakeya.Space) 1) → (∀ i : Fin n, MeasurableSet (Y i)) → (∀ i : Fin n, Y i ⊆ Metric.thickening δ (segment ℝ (x i) (x i + v i))) → ENNReal.ofReal (lam * (n : ℝ) * δ ^ 2) ≤ Finset.sum Finset.univ (fun i : Fin n => MeasureTheory.volume (Y i)) → (∀ W : Set LeanEval.Analysis.WangZahlKakeya.Space, Convex ℝ W → ENNReal.ofReal (((Set.ncard {i : Fin n | Metric.thickening δ (segment ℝ (x i) (x i + v i)) ⊆ W} : ℕ) : ℝ) * δ ^ 2) ≤ ENNReal.ofReal m * MeasureTheory.volume W) → (∀ (p w : LeanEval.Analysis.WangZahlKakeya.Space), ‖w‖ = 1 → (((Set.ncard {i : Fin n | p ∈ Y i ∧ min ‖v i - w‖ ‖v i + w‖ ≤ b} : ℕ) : ℝ)) ≤ (1 / 2 : ℝ) * (((Set.ncard {i : Fin n | p ∈ Y i} : ℕ) : ℝ))) → ENNReal.ofReal (c * δ ^ ((3 / 2 : ℝ) + α) * lam ^ K * m ^ (-K) * (n : ℝ) ^ (1 / 2 : ℝ)) ≤ MeasureTheory.volume (⋃ i : Fin n, Y i)wz_hairbrush_seedThe normalized small-error Katz–Tao convex / Frostman slab tube estimate D(1/2,0), with average δ^η shading density and essentially distinct tubes.
∀ ε : ℝ, 0 < ε → ∃ a : ℝ, 0 < a ∧ ∃ η : ℝ, 0 < η ∧ ∀ δ : ℝ, 0 < δ → δ ≤ (1 / 100 : ℝ) → ∀ (n : ℕ) (x v : Fin n → LeanEval.Analysis.WangZahlKakeya.Space) (Y : Fin n → Set LeanEval.Analysis.WangZahlKakeya.Space), 0 < n → (∀ i : Fin n, ‖v i‖ = 1) → (∀ i : Fin n, Metric.thickening δ (segment ℝ (x i) (x i + v i)) ⊆ Metric.ball (0 : LeanEval.Analysis.WangZahlKakeya.Space) 1) → (∀ i j : Fin n, i ≠ j → MeasureTheory.volume (Metric.thickening δ (segment ℝ (x i) (x i + v i)) ∩ Metric.thickening δ (segment ℝ (x j) (x j + v j))) ≤ (1 / 2 : ENNReal) * MeasureTheory.volume (Metric.thickening δ (segment ℝ (x i) (x i + v i)))) → (∀ i : Fin n, MeasurableSet (Y i)) → (∀ i : Fin n, Y i ⊆ Metric.thickening δ (segment ℝ (x i) (x i + v i))) → ENNReal.ofReal (δ ^ η * (n : ℝ) * δ ^ 2) ≤ Finset.sum Finset.univ (fun i : Fin n => MeasureTheory.volume (Y i)) → (∀ W : Set LeanEval.Analysis.WangZahlKakeya.Space, Convex ℝ W → ENNReal.ofReal (((Set.ncard {i : Fin n | Metric.thickening δ (segment ℝ (x i) (x i + v i)) ⊆ W} : ℕ) : ℝ) * δ ^ 2) ≤ ENNReal.ofReal (δ ^ (-η)) * MeasureTheory.volume W) → (∀ (u : LeanEval.Analysis.WangZahlKakeya.Space) (t r : ℝ), ‖u‖ = 1 → 0 < r → ENNReal.ofReal (((Set.ncard {i : Fin n | Metric.thickening δ (segment ℝ (x i) (x i + v i)) ⊆ (Metric.ball (0 : LeanEval.Analysis.WangZahlKakeya.Space) 1 ∩ {p : LeanEval.Analysis.WangZahlKakeya.Space | |inner ℝ u p - t| ≤ r})} : ℕ) : ℝ)) ≤ ENNReal.ofReal ((δ ^ (-η)) * (n : ℝ)) * MeasureTheory.volume (Metric.ball (0 : LeanEval.Analysis.WangZahlKakeya.Space) 1 ∩ {p : LeanEval.Analysis.WangZahlKakeya.Space | |inner ℝ u p - t| ≤ r})) → ENNReal.ofReal (a * δ ^ ((0) + ε) * ((n : ℝ) * δ ^ 2) * ((n : ℝ) * δ) ^ (-(((1 / 2 : ℝ)) : ℝ))) ≤ MeasureTheory.volume (⋃ i : Fin n, Y i)import ChallengeDeps
open LeanEval.Analysis.WangZahlKakeya
open MeasureTheory
theorem wang_zahl_kakeya_dimH {K : Set Space} (hK : IsKakeya K) :
dimH K = 3 := by
sorry
| Configuration配置 | Wall clock (min)用时（分钟） | CPU-hours used实际 CPU 小时 |
|---|---|---|
| Lean's original pipelineLean 原始流程 | 11.9 | 0.367 |
| LOT’s infrastructure (all six optimizations)LOT 基础设施（6 项优化全开） | 3.2 | 0.118 |
| Optimizations of the previous release, levels side by side (2 workers)上一版优化，各层并排检查（2 个 worker） | 5.1 | 0.235 |
| Optimizations of the previous release, level by level上一版优化，逐层检查 | 7.1 | 0.192 |
| As it ran in the proved tree (that day’s pipeline, queueing included)证明树当时实际用时（当时的流程，含排队） | 13.8 | – |
Conditions: two 20-CPU, 64 GiB containers on one host (AMD EPYC 7B13), started together on disjoint CPUs, network off, every tool and library mounted read-only; Lean leanprover/lean4:v4.35.0-rc3. The original pipeline is the unmodified official checker[3,4] run once per level; queue waits and the scheduler’s pauses between levels are not counted for either lane. Measured on 2026-10-24.条件：同一台主机（AMD EPYC 7B13）上的两个 20 核、64 GiB 容器，同时启动、CPU 不重叠，断网，所有工具和库只读挂载；Lean leanprover/lean4:v4.35.0-rc3。原始流程是未经改动的官方检查器[3,4]，每层运行一次；两条泳道都不计排队等待和层与层之间调度器的停顿。测于 2026-10-24。