從管族到證明狀態機：三維掛谷猜想的凸體轉譯、有限記憶形式化與程式化證明路線

副標題：由 Wang–Zahl 證明結構出發的生成式幾何、Witness Path 與 Proof DAG 命題

作者：Neo.K
版本：v0.1 Research Proposal / Methodological Conjecture
日期：2026-07-08

摘要

2025 年，Hong Wang 與 Joshua Zahl 公開了三維掛谷猜想（Kakeya conjecture in $\mathbb{R}^3$ ）的證明工作，其核心結果以 $\delta$ -tubes、凸集聚集、Convex Wolff axioms、多尺度分析與結構化幾何分解為中心。2026 年，Larry Guth、Hong Wang 與 Joshua Zahl 又提出一份 streamlined and simplified proof，顯著降低了原始長篇證明的表面工程複雜度。本文不重證該定理，也不聲稱已完成 Lean、Coq、Isabelle 或其他 proof assistant 中的機器驗證；本文提出的是一條新的形式化研究命題與工程路線：

三維掛谷證明的主要程式化障礙，可能不在於天價數值算力，也不在於保存所有幾何點、所有 tube 交互或所有搜索分支，而在於是否能把原證明重新編譯為正確的「證明資料結構」。

本文首先修正一個直覺性但不精確的說法：Wang–Zahl 證明中的 $\delta$ -tube 不應直接稱為嚴格凸幾何意義下的「常寬體」（constant-width body）。更精準的表示是單位線段與半徑 $\delta$ 球的 Minkowski sum，亦即一種定半徑管狀凸體、等厚管體或 segment–ball Minkowski body。此修正不削弱原直覺，反而使其更適合形式化，因為 tube 可由有限參數生成，而 Wang–Zahl 的核心論證本身又大量使用一般凸集、凸集密度與多尺度聚集結構。

本文進一步區分「數學上唯一路徑」與「形式驗證中只需保留一條成功 witness path」。掛谷條件並不宣稱每個方向只有唯一線段，Wang–Zahl 證明本身也包含 refinement、pigeonholing、子族選取、尺度選擇與存在性 witness；然而，一個 proof assistant 並不需要保存所有可能選擇分支。若某一步只需證明存在 (y) 使 (P(x,y)) 成立，則可保存一個被證明合法的 witness，並將其壓縮為後續可引用的 theorem object。由此，本文提出：

\boxed{ \text{Tube Geometry} \rightarrow \text{Parameterized Convex Objects} \rightarrow \text{Certified State Transitions} \rightarrow \text{Witness Path} \rightarrow \text{Proof DAG} }

並提出「有限記憶多尺度證明機」（Finite-Memory Multiscale Proof Machine, FMMPM）的概念架構。其核心不是暴力枚舉，而是對當前尺度、當前 tube family、當前 convex cover、當前 refinement、局部不變量與進度量進行狀態化表示；已驗證的局部中間資料可在 theorem object 或 certificate 固化後釋放。

本文最後提出一個可實作的分階段計畫：先形式化 tube 與 convex density 的最小核心，再建立尺度與漸近記號層，之後形式化有限版本的 convex cover 與 witness selection，最後才進入完整多尺度歸納。本文主張，未來最值得嘗試的並非「直接把 127 頁證明逐句翻譯成 Lean」，而是先建構：

\boxed{ \text{Wang–Zahl Proof Machine} }

亦即將原證明轉譯為一個可執行、可局部驗證、可壓縮歷史、可重播 certificate、並能由 proof assistant 最終核驗的證明狀態系統。

關鍵詞

Kakeya conjecture；三維掛谷猜想；Hong Wang；Joshua Zahl；Larry Guth；formalization；proof assistant；Lean；convex geometry； $\delta$ -tube；Minkowski sum；Convex Wolff axioms；multiscale analysis；witness path；proof DAG；finite-memory proof；programmatic proof；AI-assisted theorem proving

1. 問題背景：從「證明很長」到「資料結構是否錯了」

三維掛谷猜想的直觀敘述是：若 $E\subseteq\mathbb R^3$ 在每個方向都包含一條單位線段，則 (E) 應具有完整三維的 Hausdorff dimension；相應的定量版本則研究不同方向的細 tube 如何重疊，以及其聯集體積能縮小到何種程度。

2025 年 Wang–Zahl 的工作以 $\delta$ -tubes、凸集中的 tube 密度與多尺度結構為中心，給出三維情況的證明。其原始預印本長達 127 頁。2026 年 Guth–Wang–Zahl 又公開一份 47 頁的 streamlined proof，明確定位為 simplified proof。

對形式化研究而言，這帶來一個重要訊號：

原始證明的篇幅與人類閱讀複雜度，不必然等於形式驗證時的計算複雜度，更不必然等於需要保存的幾何資料量。

傳統直覺容易把「120 多頁的複雜幾何分析」想像成：

\text{大量空間離散化} + \text{數十億 tube} + \text{巨大交點矩陣} + \text{天價 GPU/CPU}

但這種想像很可能把兩件不同的事混在一起：

數值模擬全部幾何配置；
形式驗證一條普遍性數學推理鏈。

形式化證明的主要任務不是「把所有可能的 tube 都算一遍」，而是驗證：

\forall \mathbb T,\quad H(\mathbb T) \Rightarrow C(\mathbb T)

其中 (H) 是假設，(C) 是結論。

因此，真正問題可能不是：

我們能否算完所有幾何狀態？

而是：

我們能否找到一個足夠精確的符號表示，使 proof assistant 只需核驗定義、局部引理、存在性 witness、尺度轉換與最終推論？

這是本文的起點。

2. 第一個修正：tube 不是嚴格意義的常寬體

2.1 原始直覺

一個自然直覺是：

將 Wang–Zahl 使用的細管，轉譯成某種「常寬幾何體」，再以凸幾何物件進行程式表示。

這個方向的核心是對的，但「常寬體」一詞在凸幾何中有嚴格定義，因此需要修正。

2.2 $\delta$ -tube 的生成式表示

令 $a\in\mathbb R^3$ ， $v\in S^2$ ，並令單位線段為

L(a,v) = \{a+t v:0\le t\le 1\}.

一條半徑 $\delta$ 的 tube 可寫成

T(a,v,\delta) = \{x\in\mathbb R^3: \operatorname{dist}(x,L(a,v))\le\delta \}.

等價地，可表示為 Minkowski sum：

T(a,v,\delta) = L(a,v)\oplus \delta B_2^3,

其中 $B_2^3$ 是三維 Euclidean unit ball。

因此 tube 是一個由：

起點 (a)；
方向 (v)；
長度 (1)；
半徑 $\delta$

生成的凸體。

2.3 為何不是 constant-width body

若 $u\in S^2$ 是測量方向，則上述 capsule-like body 的寬度依賴 (u) 與 (v) 的夾角。粗略寫為：

w_T(u) = |\langle u,v\rangle| + 2\delta.

因此當 $u\perp v$ ：

w_T(u)=2\delta,

而當 $u\parallel v$ ：

w_T(u)=1+2\delta.

故：

w_T(u) \neq \text{constant}.

所以形式論文中不宜稱其為嚴格的「常寬體」。

2.4 建議術語

本文建議使用：

定半徑管狀凸體；
等厚管體；
線段–球 Minkowski 體；
Segment–Ball Minkowski Body。

其中「等厚」只表示橫向鄰域半徑固定，不表示所有方向支撐寬度相同。

2.5 修正後反而更適合形式化

這一修正並未破壞原命題，反而揭示真正有利之處：

\boxed{ T \text{ 不必儲存為點集合，而可儲存為生成參數} }

即：

T \equiv (a,v,\delta).

形式系統需要證明 membership 時，再展開：

x\in T \iff \operatorname{dist}(x,L(a,v)) \le\delta.

因此不需要 voxelization，也不需要存 tube 內部所有點。

3. 第二個修正：「唯一路徑」不是數學唯一，而是成功 witness path

3.1 掛谷條件本身不是唯一性條件

掛谷集合的核心存在性條件是：

\forall \omega\in S^2,\quad \exists L_\omega\subseteq E

使 $L_\omega$ 是方向 $\omega$ 的單位線段。

這不是：

\forall \omega,\quad \exists! L_\omega.

也就是說，同一方向可以有多條候選線段。

離散化後，若取 $\delta$ -separated directions：

\Omega_\delta = \{\omega_1,\dots,\omega_N\},

則通常只需對每個方向選一個代表 tube：

\omega_i \mapsto T_i.

因此更精準的結構是：

\forall \omega_i\in\Omega_\delta,\quad \exists T_i

而非唯一性。

3.2 Wang–Zahl 證明也不是 deterministic single path

複雜多尺度證明通常包含：

choose a scale；
select a refinement；
dyadic pigeonholing；
pass to a subcollection；
maximal family；
convex cover；
existential witness；
case split。

因此原證明在數學上並不存在一條天然唯一的 deterministic path。

3.3 但形式驗證只需保存一條成功路徑

這裡才是原直覺真正有力量之處。

假設某引理為：

\forall x,\quad H(x)\Rightarrow \exists y,\ P(x,y).

若後續證明只需要某個滿足 (P(x,y)) 的 (y)，則 proof assistant 並不需要永久保留所有候選：

y_1,y_2,\dots

只需要一個合法 witness：

[ y^*. ]

因此：

\boxed{ \text{數學上多分支} \;\not\Rightarrow\; \text{驗證時必須保存整棵搜索樹} }

而是：

\boxed{ \text{只需保存一條已被證明合法的 witness path} }

這是本文所稱：

成功 witness path 原則。

3.4 Choice 與 computability 必須區分

此處仍需嚴格區分：

\exists y,\ P(x,y)

不自動代表存在可高效執行的演算法：

y=\operatorname{compute}(x).

某些形式化步驟可能依賴：

classical choice；
noncomputable definition；
compactness；
supremum / infimum；
measure-theoretic existence。

因此本文主張的不是：

Wang–Zahl 證明天然就是高效可執行程式。

而是：

它可能被表示為低歷史記憶需求的證明狀態轉換，即使部分 witness 是非計算性的。

這一區分非常重要。

4. 核心命題：證明不是巨大幾何資料庫，而是可壓縮狀態機

本文提出：

命題 A：生成式幾何壓縮命題

對 Wang–Zahl 類型的 tube/convex-set 論證，相當一部分幾何物件可由有限參數、函數定義或 predicate 表示，而非顯式點集表示：

G = (\text{primitive},\text{parameters},\text{transform}).

例如：

T_i=(a_i,v_i,\delta_i),

[ B(c,r), ]

\text{Slab}(n,b,w),

[ P=A(P_0)+b. ]

若此命題在主要證明物件上成立，則記憶體需求更接近「物件描述複雜度」而不是「幾何解析度下的點數」。

命題 B：有限歷史證明命題

若一個多尺度證明可分解為：

S_0 \xrightarrow{M_0} S_1 \xrightarrow{M_1} \cdots \xrightarrow{M_{k-1}} S_k,

且每一步都有局部 certificate：

C_i: \operatorname{Valid}(S_i) \Rightarrow \operatorname{Valid}(S_{i+1}),

則在 $C_i$ 已被 kernel 驗證並固化為 theorem object 後，執行層未必需要永久保存 $S_i$ 的全部暫存資料。

理想化而言：

\operatorname{RAM} \approx O( |S_i| + |C_i| + |\text{active dependencies}| ),

而非：

O\left( \sum_{j=0}^{i}|S_j| \right).

命題 C：Proof DAG 優於 Search Tree 命題

人類探索證明可能形成巨大搜索樹：

\mathcal T_{\mathrm{search}}.

但最終形式化證明通常可壓縮成有向無環圖：

\mathcal G_{\mathrm{proof}}.

同一 lemma 可被多次引用而不重複展開全部推導。

因此：

\boxed{ \text{探索成本} \neq \text{最終驗證成本} }

這可能是大型數學證明程式化時最容易被忽略的區分之一。

5. 從 tube family 到 convex density：為何凸體語言是天然接口

Wang–Zahl 的 2025 工作並不是只研究單條 tube 的局部幾何，而是研究 tube family 在共同凸集中的聚集。

令 $\mathbb T$ 為 tube family， $K\subseteq\mathbb R^3$ 為凸集。可定義：

\mathbb T[K] = \{T\in\mathbb T:T\subseteq K\}.

凸集中的 tube density 可寫成：

\Delta(\mathbb T,K) = \frac{ \sum_{T\in\mathbb T[K]} |T| }{ |K| }.

再考慮所有凸集上的最大密度：

\Delta_{\max}(\mathbb T) = \sup_{K\text{ convex}} \Delta(\mathbb T,K).

這種語言對形式化有一個重要優點：

證明不需要永久維護所有 pairwise intersection；它可在更高層以「某凸集容納多少 tube mass」作 aggregate invariant。

這暗示一種資料結構轉換：

\text{pairwise geometry} \rightarrow \text{regional aggregate certificate}.

例如，不保存：

I_{ij} = \mathbf 1[T_i\cap T_j\neq\varnothing]

的完整 $N\times N$ 矩陣，而保存：

n_K = \#\{T:T\subseteq K\},

或其 measure-weighted 版本。

當然，這不表示所有 pairwise 幾何都能消除；某些引理仍可能需要 incidence relation。但它顯示：

\boxed{ \text{證明使用的統計量} \text{可能比原始幾何關係矩陣低維得多} }

6. 提議：Wang–Zahl Proof Machine

本文提出將證明重構為一個抽象機器。

6.1 狀態

令第 (k) 步狀態為：

S_k = ( \delta_k, \rho_k, \mathbb T_k, \mathbb C_k, \mathbb G_k, \mathbb Y_k, \mathcal R_k, \mathcal I_k, \Theta_k ).

各欄位可理解為：

$\delta_k$ ：當前細尺度；
$\rho_k$ ：中介或粗尺度；
$\mathbb T_k$ ：當前 tube family；
$\mathbb C_k$ ：當前 convex family / cover；
$\mathbb G_k$ ：grain-like structures；
$\mathbb Y_k$ ：shading / localized subsets；
$\mathcal R_k$ ：refinement relations；
$\mathcal I_k$ ：已知 invariants；
$\Theta_k$ ：誤差、指數、常數與漸近參數。

注意：此狀態只是概念架構，不宣稱與原論文符號一一對應。

6.2 轉換

每個證明動作表示為：

M_j:S_k\mapsto S_{k+1}.

例如：

M_{\mathrm{refine}}, \quad M_{\mathrm{pigeonhole}}, \quad M_{\mathrm{cover}}, \quad M_{\mathrm{rescale}}, \quad M_{\mathrm{select}}, \quad M_{\mathrm{contradict}}.

每個 Move 必須攜帶規格：

\operatorname{Pre}_j(S)

與：

\operatorname{Post}_j(S,S').

形式化目標：

\forall S,\quad \operatorname{Valid}(S) \land \operatorname{Pre}_j(S) \Rightarrow \exists S', \operatorname{Post}_j(S,S') \land \operatorname{Valid}(S').

6.3 不變量

候選不變量包括：

\delta_k\in(0,1],

\mathbb T_k \subseteq \mathcal T(\delta_k),

\operatorname{Convex}(K) \quad \forall K\in\mathbb C_k,

\Delta_{\max}(\mathbb T_k) \le C\delta_k^{-\varepsilon},

以及 refinement 關係：

\mathbb T_{k+1} \preceq \mathbb T_k.

真正形式化時，需依 streamlined proof 的實際 theorem dependencies 重建，不應直接照本文猜測硬編。

7. 有限記憶證明：到底可以丟掉哪些資料？

7.1 三種資料

應區分：

A. Kernel-level proof object

最終 kernel 驗證所需 theorem term、常數、定義與依賴。

B. Construction-level certificate

某一步產生 witness 或 refinement 的最小證書。

C. Search-time scratch data

AI、SAT/SMT、數值程序或 heuristic 搜尋時產生的大量暫存資料。

本文最核心的工程假說是：

\boxed{ C \text{ 被驗證後，許多 } B,C \text{ 層暫存可釋放} }

更精確地說，不能隨意刪除 kernel 仍需 replay 的依賴，但可以避免保存探索過程。

7.2 例：maximal subfamily

假設需要選擇 maximal essentially distinct family：

\mathbb F^\* \subseteq \mathbb F.

搜索過程可能嘗試大量候選：

\mathbb F_1,\dots,\mathbb F_M.

但最終證明只需要：

$\mathbb F^\*\subseteq\mathbb F$ ；
pairwise essential distinction；
maximality certificate。

因此：

\{\mathbb F_1,\dots,\mathbb F_M\}

不必進入最終 proof artifact。

7.3 例：尺度選擇

假設 dyadic scales：

\delta \le \rho \le 1.

人類證明可能說：

由 pigeonholing，可選某尺度 $\rho$ 使……

程序探索時可測試多個 $\rho$ ，但最終只需一個：

\rho^\*

以及：

\operatorname{GoodScale}(\rho^\*).

因此驗證物件是：

(\rho^\*,C_{\rho^\*})

而不是所有失敗尺度。

8. 為何「不需要天價算力」是合理命題，但不是既成事實

本文支持以下判斷：

\boxed{ \text{形式化 Wang–Zahl 證明} \text{ 很可能不是以天價浮點算力為主要瓶頸} }

理由有四。

8.1 普遍證明不是枚舉

目標是證明：

\forall\mathbb T,\ H(\mathbb T)\Rightarrow C(\mathbb T),

不是對所有 finite encoding 的 tube family 一一測試。

8.2 幾何物件可生成

tube：

T=(a,v,\delta)

而不是 point cloud。

8.3 大量步驟是符號推理

例如：

inclusion；
convexity；
measure inequality；
monotonicity；
scaling；
affine transformation；
cardinality bound；
existence；
induction。

這些通常更依賴 theorem library 與 term elaboration，而非 GPU FLOPS。

8.4 歷史可壓縮

成功 witness 與 theorem DAG 可消除失敗探索分支。

8.5 但不能提前承諾低成本

以下問題仍可能造成巨大工程成本：

proof term blow-up；
typeclass synthesis；
coercion explosion；
measure-theoretic rewriting；
nonlinear real arithmetic；
repeated normalization；
asymptotic constants；
nested $\varepsilon$ -dependencies；
finite/infinite bridge；
classical choice；
compilation memory；
kernel replay time。

所以更精確的結論是：

\boxed{ \text{沒有理由先假定需要天價數值算力； 但形式化工程成本仍可能極高} }

9. 最大真正瓶頸：不是 tube，而是分析語言

將 tube 寫成：

structure Tube where
  base : EuclideanSpace ℝ (Fin 3)
  dir  : EuclideanSpace ℝ (Fin 3)
  radius : ℝ
  hdir : ‖dir‖ = 1
  hradius : 0 < radius

並不困難。

真正困難可能是後面：

Lebesgue measure；
Hausdorff dimension；
Minkowski dimension；
measurable sets；
convex sets；
affine images；
supremum over convex families；
$O(\delta^{-\varepsilon})$ ；
$\lesssim$ 、 $\sim$ ；
multi-parameter asymptotics；
induction on scales；
nested refinements；
almost-everywhere statements。

因此：

\boxed{ \text{Tube Definition} \ll \text{Analytic Infrastructure} }

10. 漸近記號是形式化中的高風險區

人類論文大量使用：

A\lesssim B, \quad A\sim B, \quad A\lessapprox B.

但 proof assistant 必須知道：

A\le C B

中的：

(C) 依賴誰；
是否依賴 $\delta$ ；
是否依賴 $\varepsilon$ ；
是否依賴 dimension；
在何範圍成立。

因此建議建立顯式 dependency signature：

C=C(d,\varepsilon,C_0).

甚至定義：

BoundedBy deps A B

表示存在常數 (C)，且 (C) 只能依賴 deps。

若不先解決這一層，整個大型證明可能因 constant bookkeeping 失控。

11. 「唯一成功路徑」的更精準數學表述

本文將原始直覺正式超譯為：

Witness-Path Compression Principle

考慮證明程序中的多值轉換：

S_{k+1} \in F(S_k).

其中 $F(S_k)$ 可能有多個合法後繼。

若最終 theorem 只要求：

\exists (S_0,\dots,S_n)

滿足：

S_{k+1}\in F(S_k)

及：

\operatorname{Terminal}(S_n),

則形式化 artifact 不必包含所有：

\prod_k |F(S_k)|

條可能路徑。

只需：

\pi^\* = (S_0,S_1,\dots,S_n)

及逐步 certificate：

C_k: S_{k+1}\in F(S_k).

因此：

\boxed{ \text{Branching Proof Search} \rightarrow \text{Linear Witness Trace} }

若中間 lemma 被共享，則更一般化為：

\boxed{ \text{Search Tree} \rightarrow \text{Proof DAG} }

這就是「唯一的路徑」直覺的精準版本。

12. 可程式化不等於可計算證明

本文強調三層區分：

12.1 Formalizable

可在 Lean/Coq/Isabelle 中表述並驗證。

12.2 Programmatically constructible

witness 或證明步驟可由程序生成。

12.3 Efficiently computable

程序在可接受時間與記憶體內完成。

三者關係：

\text{efficiently computable} \Rightarrow \text{programmatically constructible}

但不一定：

\text{formalizable} \Rightarrow \text{efficiently computable}.

Wang–Zahl 路線最合理的初始目標應是：

\boxed{ \text{Formalizable} + \text{Partially Programmatically Constructible} }

而不是一開始要求全證明 executable。

13. Streamlined proof 改變了實作優先順序

2025 年原始 Wang–Zahl 預印本為 127 頁；2026 年 Guth–Wang–Zahl 公開 47 頁 streamlined and simplified proof。

因此未來工程不應採取：

\text{Original 127 pages} \rightarrow \text{逐句 Lean 化}.

更合理的是：

\boxed{ \text{2026 Streamlined Proof} \rightarrow \text{Dependency Graph} \rightarrow \text{Minimal Formal Core} }

而 2025 原始證明則作為：

缺失細節查詢源；
定義來源；
lemma provenance；
複雜情況備援；
幾何直覺資料庫。

14. 建議的形式化分層

Layer 0：基礎 Euclidean Geometry

需要：

\mathbb R^3, \quad \langle x,y\rangle, \quad \|x\|, \quad \operatorname{dist}.

Layer 1：Segment 與 Tube

定義：

L(a,v) = \{a+tv:0\le t\le1\},

T(a,v,\delta) = \{x:\operatorname{dist}(x,L(a,v))\le\delta\}.

證明：

closedness；
convexity；
measurability；
translation covariance；
rotation covariance；
scaling relation。

Layer 2：Tube Family 與 Direction Separation

定義：

\angle(v_i,v_j)\ge c\delta.

以及 finite family：

\mathbb T:\text{Finset Tube}.

Layer 3：Convex Container

定義：

\mathbb T[K] = \{T:T\subseteq K\}.

證明 inclusion、monotonicity 等。

Layer 4：Density

\Delta(\mathbb T,K).

需決定 tube mass 使用：

volume；
nominal $\delta^2$ ；
exact measure；
normalized weight。

Layer 5：Scale Algebra

形式化：

0<\delta\le\rho\le1.

dyadic scales：

\rho=2^{-k}.

建立 rescale API。

Layer 6：Refinement

將：

pass to a large subcollection

形式化成：

\mathbb T' \subseteq \mathbb T

加 quantitative survival：

|\mathbb T'| \ge c|\mathbb T|.

Layer 7：Pigeonholing

先形式化有限 dyadic pigeonhole lemma。

Layer 8：Convex Cover / Grain-like Objects

逐步加入更複雜幾何結構。

Layer 9：Multiscale Transition System

把證明真正組裝成：

S_k\to S_{k+1}.

Layer 10：Final Analytic Bridge

從 tube estimate 推回：

Minkowski dimension；
Hausdorff dimension。

15. 建議不要第一天就碰 Hausdorff dimension

這是重要工程策略。

最終定理很宏大，但第一階段不應從：

theorem kakeya_hausdorff_dim_three ...

開始。

應先做：

theorem tube_is_convex ...

再：

theorem tube_affine_covariant ...

再：

theorem convex_density_monotone ...

再：

theorem refinement_preserves_direction_separation ...

大型形式化專案最危險的錯誤是：

從最終 theorem statement 開始，卻沒有中間 API。

16. 最小可行原型：不是證明掛谷，而是證明「這條路能走」

本文建議第一個 MVP 只做：

MVP-1：Tube as Parameterized Convex Body

完成：

T(a,v,\delta) = L(a,v)\oplus\delta B.

驗證：

convex；
measurable；
bounded。

MVP-2：Finite Direction Family

建立：

\Omega_\delta

的 finite approximation。

不是用來證明完整掛谷，而是測試資料結構。

MVP-3：Witness Selection

形式化：

\forall\omega\in\Omega, \exists T,\ \operatorname{dir}(T)=\omega

推出某個 choice map：

f:\Omega\to\text{Tube}.

比較：

computable finite choice；
classical choice。

MVP-4：Convex Density

形式化：

\Delta(\mathbb T,K).

MVP-5：Proof DAG Export

將已證 lemma 依賴輸出成 DAG。

測量：

theorem count；
proof term size；
peak RAM；
elaboration time；
kernel replay time。

這一步將第一次真正檢驗「不需要天價算力」命題。

17. 記憶體複雜度：應測量什麼

本文不預設低記憶必然成立，而提出可驗證指標。

17.1 Peak active state

M_{\mathrm{active}} = \max_k |S_k|.

17.2 Historical retention

M_{\mathrm{history}} = \left| \bigcup_{j\le k} \text{retained}(S_j) \right|.

理想目標：

M_{\mathrm{history}} \not\sim \sum_j|S_j|.

17.3 Proof DAG size

|\mathcal G_{\mathrm{proof}}|.

17.4 Search-to-proof compression ratio

\mathrm{CPR} = \frac{ |\mathcal T_{\mathrm{search}}| }{ |\mathcal G_{\mathrm{proof}}| }.

若：

\mathrm{CPR}\gg1,

則證明探索很昂貴，但最終 artifact 可大幅壓縮。

17.5 Certificate replay cost

C_{\mathrm{replay}}.

若 proof 太壓縮但 kernel replay 極慢，也不算成功。

18. AI 在此計畫中的角色

AI 的角色不是代替 proof kernel。

最合理架構：

\boxed{ \text{AI proposes} \rightarrow \text{Program constructs} \rightarrow \text{Kernel verifies} }

18.1 AI 解析自然語言證明

把：

by dyadic pigeonholing, choose a scale...

轉成候選形式 schema。

18.2 AI 找出隱含依賴

例如一句：

clearly $T\subseteq K$

背後可能需要：

norm inequality；
coordinate bound；
convexity；
triangle inequality。

18.3 AI 生成局部 witness

在有限問題上由程序搜尋：

[ y^*. ]

18.4 AI 做 dependency minimization

從巨大 lemma set 找出最小依賴。

18.5 AI 做失敗診斷

當 Lean proof fail 時分類：

缺 theorem；
coercion；
measure；
arithmetic；
type mismatch；
wrong abstraction。

19. Compute-First 與 Formalize-First 的結合

本文受到一種更廣義的「計算即逼近」方法論啟發，但在此問題上需做變形。

不是：

\text{大量數值計算} \rightarrow \text{猜定理}.

而是：

\text{嘗試形式化} \rightarrow \text{暴露隱含依賴} \rightarrow \text{重構證明} \rightarrow \text{再形式化}.

可寫為：

F_0 \rightarrow E_0 \rightarrow R_1 \rightarrow F_1 \rightarrow E_1 \rightarrow\cdots

其中：

$F_k$ ：第 (k) 版 formalization；
$E_k$ ：error / obstruction；
$R_k$ ：proof restructuring。

所以：

\boxed{ \text{形式化失敗本身就是證明結構探測器} }

20. 一個更激進的超譯：證明本身是一種壓縮演算法

本文提出更一般命題：

一個成功數學證明，可以被理解為把無限或巨大可能空間壓縮成有限依賴結構的演算法。

掛谷問題的配置空間巨大：

\mathcal X = \{\text{all admissible tube configurations}\}.

證明不枚舉：

x_1,x_2,\dots

而是找到不變量：

I_1,\dots,I_m

使：

H(x) \Rightarrow I_1(x) \Rightarrow \cdots \Rightarrow C(x).

因此證明本身就是：

\boxed{ \text{configuration space} \rightarrow \text{invariant compression} }

若此觀點成立，則形式化的真正任務不是「把空間算完」，而是「忠實編碼壓縮映射」。

21. 有限記憶多尺度證明機（FMMPM）

本文正式提出：

Finite-Memory Multiscale Proof Machine

其狀態：

S_k = ( \text{Scale}, \text{Objects}, \text{Relations}, \text{Invariants}, \text{Witnesses}, \text{Obligations} ).

Transition

S_k \xrightarrow{M} S_{k+1}.

Certificate

C_M: \operatorname{Valid}(S_k) \Rightarrow \operatorname{Valid}(S_{k+1}).

Garbage Collection

當 $S_k$ 的資訊已被：

theorem object；
compressed invariant；
witness certificate

完全吸收後，允許釋放非必要 scratch data。

Terminal Condition

\operatorname{Contradiction}(S_n)

或：

\operatorname{Goal}(S_n).

22. 可能的 Lean 抽象草圖

以下只是概念伪代码：

structure Tube3 where
  base   : E3
  dir    : E3
  radius : ℝ
  hdir   : ‖dir‖ = 1
  hr     : 0 < radius

def Tube3.carrier (T : Tube3) : Set E3 :=
  {x | dist x (segmentSet T.base (T.base + T.dir)) ≤ T.radius}

theorem tube_convex (T : Tube3) :
    Convex ℝ T.carrier := by
  ...

structure MultiScaleState where
  fineScale   : ℝ
  coarseScale : ℝ
  tubes       : Finset Tube3
  invariants  : InvariantBundle
  obligations : Finset Goal

structure MoveCertificate (S S' : MultiScaleState) : Prop where
  preserve : Valid S → Valid S'
  progress : Progress S S'

def ProofPath :=
  List MultiScaleState

真正實作時未必使用 Finset Tube3；某些 theorem 必須處理集合、可測 family、indexed family 或其他抽象結構。但此草圖展示的是資料結構方向。

23. 為何不建議 voxelization

若把 $[0,1]^3$ 以解析度 (h) 離散：

N\sim h^{-3}.

再儲存 tube occupancy：

O(|\mathbb T|h^{-3}),

很快爆炸。

而生成式 tube：

T_i=(a_i,v_i,\delta)

只需 (O(1)) 參數。

所以：

\boxed{ \text{Voxel Geometry} \text{ 是錯誤的第一表示} }

至少對普遍形式證明而言如此。

24. 反例：何時仍可能需要大量資料

本文不能過度樂觀。

24.1 Explicit finite search

若某 lemma 最終化成大型有限組合搜索，資料仍可能爆炸。

24.2 Massive incidence graph

若必須顯式保存：

G=(\mathbb T,\mathbb T,E)

且：

|E|\sim|\mathbb T|^2,

則仍昂貴。

24.3 Proof term duplication

不良 formalization 可能把共享 lemma 重複 inline。

24.4 Simplifier blow-up

自動重寫可能造成 expression explosion。

24.5 Nonlinear arithmetic

大量實閉域推理可能昂貴。

因此有限記憶不是免費結果，而是架構目標。

25. 可證偽性：如何判斷本文命題錯了

本文提出的工程命題必須可被反駁。

若實驗發現：

每個 multiscale step 都需要保留大量全歷史上下文；
witness certificate 幾乎與完整搜索樹同大；
convex density 無法壓縮 incidence data；
proof DAG 幾乎退化成巨大 tree；
streamlined proof 的每一步都依賴龐大全域 analytic state；
kernel replay cost 超過可接受範圍；

則：

\boxed{ \text{有限記憶形式化假說被削弱} }

甚至否定。

26. 實驗路線圖

Phase I：語義轉譯

目標：

\text{paper notation} \rightarrow \text{typed objects}.

產物：

glossary；
dependency map；
object taxonomy。

Phase II：幾何 MVP

完成：

segment；
tube；
Minkowski neighborhood；
convexity；
measurability。

Phase III：Convex density MVP

完成：

\mathbb T[K], \quad \Delta(\mathbb T,K).

Phase IV：Witness path engine

建立：

existential witness object；
certificate；
branch pruning；
replay。

Phase V：Multiscale state machine

建立：

S_k\to S_{k+1}.

Phase VI：Streamlined proof mapping

對 2026 版本逐 lemma 建：

L_i \mapsto \text{formal dependencies}.

Phase VII：完整 theorem integration

最後才嘗試 Kakeya theorem。

27. 最重要的策略修正：不要「翻譯論文」，要「編譯證明」

自然語言論文：

P_{\mathrm{NL}}

不應直接逐句翻成：

P_{\mathrm{Lean}}.

應先經中介表示：

P_{\mathrm{NL}} \rightarrow IR_{\mathrm{proof}} \rightarrow P_{\mathrm{Lean}}.

其中 proof IR 包括：

typed objects；
hypotheses；
witnesses；
invariants；
transitions；
dependencies；
asymptotic scopes。

因此：

\boxed{ \text{Paper} \rightarrow \text{Proof IR} \rightarrow \text{Proof Assistant} }

這可能比逐句翻譯穩定得多。

28. Proof IR 的候選格式

lemma_id: multiscale_step_17

inputs:
  state: S
  scale:
    fine: delta
    coarse: rho

assumptions:
  - 0 < delta
  - delta <= rho
  - rho <= 1
  - convex_wolff_bound T

witness:
  type: refinement
  name: T_prime

guarantees:
  - T_prime ⊆ T
  - cardinality_lower_bound
  - invariant_preserved

dependencies:
  - dyadic_pigeonhole
  - refinement_transitivity
  - density_monotonicity

此 IR 可由：

人類；
AI；
parser；
theorem prover bridge

共同維護。

29. 本文最核心的五個主張

主張一

\boxed{ \delta\text{-tube 應視為生成式定半徑管狀凸體，而非 point cloud} }

主張二

\boxed{ \text{數學多分支} \neq \text{最終證明必須保存多分支} }

主張三

\boxed{ \text{形式驗證可保存成功 witness path，而非完整 search tree} }

主張四

\boxed{ \text{Wang–Zahl 類多尺度證明可嘗試轉為 certified state machine} }

主張五

\boxed{ \text{主要瓶頸可能是定義、分析庫與證明 IR，而非天價浮點算力} }

30. 更進一步的理論命題：普遍證明的「資料遺忘權」

本文提出一個超出 Kakeya 的一般命題。

證明資料遺忘命題

若某中間資料 $D_k$ 的全部後續語義作用，已被 theorem object $L_k$ 完整吸收：

D_k \vdash L_k,

且後續只依賴：

[ L_k ]

而不再依賴 $D_k$ 的內部結構，則執行系統應允許：

D_k \rightarrow \varnothing

於 runtime scratch layer。

這不是刪除數學依賴，而是：

\boxed{ \text{用已驗證語義壓縮取代原始計算歷史} }

這可稱為：

Proof-State Semantic Garbage Collection

即：

證明狀態語義垃圾回收。

31. 與 AI 主導數學研究的連結

未來 AI theorem systems 很可能面臨一個問題：

\text{探索速度} \uparrow \Rightarrow \text{中間狀態} \uparrow\uparrow.

若每次嘗試都永久保存，則記憶體與上下文爆炸。

因此需要：

\text{Search} \rightarrow \text{Verify} \rightarrow \text{Compress} \rightarrow \text{Forget} \rightarrow \text{Continue}.

可寫為：

\boxed{ \text{計算} \rightarrow \text{證明} \rightarrow \text{語義壓縮} \rightarrow \text{遺忘} \rightarrow \text{下一輪計算} }

三維 Kakeya 可能成為測試此架構的高價值案例。

32. 研究風險

32.1 對原證明結構誤判

本文尚未完成逐 lemma dependency audit。

32.2 現有數學庫不足

需要補大量 analytic infrastructure。

32.3 非計算性 witness

可能限制 executable extraction。

32.4 Proof IR 設計失敗

中介表示可能比原證明更複雜。

32.5 Streamlined proof 仍高度困難

47 頁不代表容易。

33. 特別聲明

本文：

不是 Wang–Zahl 定理的新證明；
不是已完成的形式化證明；
不聲稱三維 Kakeya 已在 Lean 中被驗證；
不聲稱形式化必然低成本；
不聲稱 witness 一定可計算；
不將 $\delta$ -tube 誤稱為嚴格 constant-width body。

本文是一個：

\boxed{ \text{形式化研究命題} + \text{證明工程架構} + \text{未來實驗路線} }

34. 結論

本文起於一個直覺：

Wang–Zahl 證明中的 tube，若改以可參數化凸幾何物件表示，並考慮掛谷條件與證明過程中的 witness 選取，是否可能讓整個證明比想像中更適合程式化？

經修正後，本文得到更精準的答案：

第一，tube 不是嚴格常寬體，但可表示為：

T(a,v,\delta) = L(a,v)\oplus\delta B.

第二，證明不是數學上的唯一 deterministic path，但形式 artifact 可以只保存一條成功 witness path。

第三，不必保存 tube 內所有點，也不必預設保存完整 pairwise relation matrix。

第四，多尺度證明可嘗試重構為：

S_k \xrightarrow{M_k} S_{k+1}

的 certified state transition。

第五，搜索樹可壓縮為：

\mathcal T_{\mathrm{search}} \rightarrow \mathcal G_{\mathrm{proof}}.

第六，已驗證的局部中間狀態可能透過 semantic garbage collection 釋放。

因此本文最終提出：

\boxed{ \text{Wang–Zahl Proof} \approx \text{Parameterized Geometry} + \text{Multiscale State Machine} + \text{Witness Path} + \text{Proof DAG} + \text{Kernel Verification} }

真正值得未來嘗試的，不是把長篇論文粗暴地逐句翻譯成 Lean，也不是以 voxel 暴力模擬所有 tube，而是建立一個：

\boxed{ \textbf{Wang–Zahl Proof Machine} }

更廣義地說，這個計畫真正測試的是另一個命題：

大型現代數學證明是否可以被重新編譯為有限活動狀態、局部可驗證轉換、可壓縮 witness 與共享依賴 DAG？

若答案為是，則三維掛谷猜想不只是一個被證明的幾何測度定理；它還可能成為下一代 AI 輔助形式數學、程式化證明與有限記憶推理系統的重要試驗場。

附錄 A：一句話版本

不要把三維掛谷證明想成「保存所有 tube 並暴力算完」，而應把 tube 編碼成生成式凸體，把多尺度論證編譯成證明狀態機，只保留成功 witness、局部 certificate 與 Proof DAG。

附錄 B：最小實驗 checklist

在 Lean 中定義三維 Euclidean segment
定義 $\delta$ -tube
證明 tube convex
證明 tube measurable
定義 finite tube family
定義 direction separation
定義 convex container
定義 $\mathbb T[K]$
定義 convex density
建立 finite witness choice
建立 proof-path certificate
輸出 theorem dependency DAG
測量 peak RAM
測量 proof term size
測量 kernel replay time
對 2026 streamlined proof 做 dependency audit
選一個真正 multiscale lemma 作第一個大型形式化測試

附錄 C：建議專案目錄

kakeya-proof-machine/
├── README.md
├── lakefile.lean
├── Kakeya/
│   ├── Geometry/
│   │   ├── Segment.lean
│   │   ├── Tube.lean
│   │   ├── MinkowskiBody.lean
│   │   └── ConvexContainer.lean
│   ├── Measure/
│   │   ├── TubeMeasure.lean
│   │   ├── UnionMeasure.lean
│   │   └── Density.lean
│   ├── Scale/
│   │   ├── Dyadic.lean
│   │   ├── Rescale.lean
│   │   └── Asymptotics.lean
│   ├── Family/
│   │   ├── DirectionSeparated.lean
│   │   ├── Refinement.lean
│   │   └── Pigeonhole.lean
│   ├── Machine/
│   │   ├── State.lean
│   │   ├── Move.lean
│   │   ├── Certificate.lean
│   │   └── ProofPath.lean
│   ├── WZ/
│   │   ├── Glossary.lean
│   │   ├── DependencyMap.md
│   │   └── Streamlined/
│   └── Main.lean
└── tools/
    ├── proof_dag.py
    ├── memory_probe.py
    └── ir_compiler.py

參考文獻

Wang, H.; Zahl, J. Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions. arXiv:2502.17655, 2025.
Guth, L. Introduction to the proof of the Kakeya conjecture. arXiv:2505.07695, 2025.
Guth, L. Outline of the Wang–Zahl proof of the Kakeya conjecture in $\mathbb R^3$ . arXiv:2508.05475, 2025.
Guth, L.; Wang, H.; Zahl, J. A streamlined proof of the Kakeya set conjecture in $\mathbb R^3$ . arXiv:2601.14411, 2026.
Guth, L. The Kakeya conjecture, after Wang and Zahl. arXiv:2604.03416, 2026.
Wang, H.; Zahl, J. Sticky Kakeya sets and the sticky Kakeya conjecture. Journal of the American Mathematical Society, 2026.

從管族到證明狀態機_三維掛谷猜想的凸體轉譯與有限記憶形式化_v0.1

從管族到證明狀態機：三維掛谷猜想的凸體轉譯、有限記憶形式化與程式化證明路線

摘要

關鍵詞

1. 問題背景：從「證明很長」到「資料結構是否錯了」

2. 第一個修正：tube 不是嚴格意義的常寬體

2.1 原始直覺

2.2 δ\deltaδ-tube 的生成式表示

2.3 為何不是 constant-width body

2.4 建議術語

2.5 修正後反而更適合形式化

3. 第二個修正：「唯一路徑」不是數學唯一，而是成功 witness path

3.1 掛谷條件本身不是唯一性條件

3.2 Wang–Zahl 證明也不是 deterministic single path

3.3 但形式驗證只需保存一條成功路徑

3.4 Choice 與 computability 必須區分

4. 核心命題：證明不是巨大幾何資料庫，而是可壓縮狀態機

命題 A：生成式幾何壓縮命題

命題 B：有限歷史證明命題

命題 C：Proof DAG 優於 Search Tree 命題

5. 從 tube family 到 convex density：為何凸體語言是天然接口

6. 提議：Wang–Zahl Proof Machine

6.1 狀態

6.2 轉換

6.3 不變量

7. 有限記憶證明：到底可以丟掉哪些資料？

7.1 三種資料

A. Kernel-level proof object

B. Construction-level certificate

C. Search-time scratch data

7.2 例：maximal subfamily

7.3 例：尺度選擇

8. 為何「不需要天價算力」是合理命題，但不是既成事實

8.1 普遍證明不是枚舉

8.2 幾何物件可生成

8.3 大量步驟是符號推理

8.4 歷史可壓縮

8.5 但不能提前承諾低成本

9. 最大真正瓶頸：不是 tube，而是分析語言

10. 漸近記號是形式化中的高風險區

11. 「唯一成功路徑」的更精準數學表述

Witness-Path Compression Principle

12. 可程式化不等於可計算證明

12.1 Formalizable

12.2 Programmatically constructible

12.3 Efficiently computable

13. Streamlined proof 改變了實作優先順序

14. 建議的形式化分層

Layer 0：基礎 Euclidean Geometry

Layer 1：Segment 與 Tube

Layer 2：Tube Family 與 Direction Separation

Layer 3：Convex Container

Layer 4：Density

Layer 5：Scale Algebra

Layer 6：Refinement

Layer 7：Pigeonholing

Layer 8：Convex Cover / Grain-like Objects

Layer 9：Multiscale Transition System

Layer 10：Final Analytic Bridge

15. 建議不要第一天就碰 Hausdorff dimension

16. 最小可行原型：不是證明掛谷，而是證明「這條路能走」

MVP-1：Tube as Parameterized Convex Body

MVP-2：Finite Direction Family

MVP-3：Witness Selection

MVP-4：Convex Density

MVP-5：Proof DAG Export

17. 記憶體複雜度：應測量什麼

17.1 Peak active state

17.2 Historical retention

17.3 Proof DAG size

17.4 Search-to-proof compression ratio

17.5 Certificate replay cost

18. AI 在此計畫中的角色

18.1 AI 解析自然語言證明

18.2 AI 找出隱含依賴

18.3 AI 生成局部 witness

18.4 AI 做 dependency minimization

18.5 AI 做失敗診斷

19. Compute-First 與 Formalize-First 的結合

20. 一個更激進的超譯：證明本身是一種壓縮演算法

2.2 $\delta$ -tube 的生成式表示