形式證明不等於過程證明：Theoremhood 與 Process Completeness

系列：形式封閉與過程完備：AI 數學證明的下一步問題
Paper 01
作者：Neo.K / EveMissLab Research Series
版本：v0.1 — 2026-09-11

機構： EveMissLab／一言諾科技有限公司
日期： 2026-09-11

摘要

現代形式化數學通常把「證明完成」理解為：在一套明確的形式系統中，某個命題具有可驗證的 proof term，且該 proof term 能通過 kernel checking。這種標準極其重要，並且大幅降低了紙面證明中的遺漏、符號錯置與局部推理錯誤。然而，當研究問題本身涉及動態過程、逐步生成、無限階構造、極限轉移、對角實現、存在性選擇或跨尺度演化時，單純的 theoremhood 並不自動等價於 process completeness。

本文提出一個基本區分：

\boxed{ \text{Theorem Closure} \neq \text{Process Completeness} }

前者回答「結論是否能從形式前提推出」；後者則要求進一步回答「每一個狀態是否真的由上一個狀態沿合法箭頭生成」、「有限階段是否形成同一條可延續路徑」、「極限物件是否來自原過程本身，而不是由新的 completion operator 事後實現」，以及「存在性證明是否對應某種可構造或可計算的生成程序」。

本文建立五層審計框架：Kernel Validity、Specification Validity、Arrow Validity、Trace Validity 與 Computational Realizability，並提出 Process-Complete Proof 的初步形式定義。本文的核心目的不是否定形式化證明，而是指出：對某些問題而言，形式化證明是必要條件，但仍不是全部研究義務。若未把「下一步為什麼是下一步」正式納入規格，proof assistant 可以完全正確地驗證一個仍具有過程語義缺口的命題。

關鍵詞

形式化證明、Lean、過程完備性、箭頭合法性、trajectory、same-parent path、存在性證明、對角化、極限、Classical.choice、可計算性、AI 數學、proof ontology

1. 問題：一個被證明的命題，是否已經等於一個被完成的過程？

假設某個形式系統證明：

\Gamma \vdash T.

在標準 proof-theoretic 意義下，只要 proof term 可由可信 kernel 驗證，則 $T$ 是相對於 $\Gamma$ 的定理。

這個判準非常清楚：

\operatorname{ValidProof}(\Gamma,T)=1.

然而，當 $T$ 描述的是一個動態過程，例如：

S_0\to S_1\to S_2\to\cdots,

問題就不再只有：

\Gamma\vdash T

是否成立。

還存在另一組問題：

S_n\to S_{n+1}

究竟是哪一種箭頭？

是否存在同一個生成規則？

是否所有 $S_n$ 屬於同一條 parent-consistent path？

是否最後的極限物件真的是這條 path 的極限？

是否某個「存在」只是形式系統中可選取，而不是可以由過程實際生成？

因此，本文首先提出：

定理成立與過程完成是兩個不同層級的判斷。

2. 第一個區分：Theorem Closure

定義一個形式理論：

\mathcal T=(\mathcal L,\mathcal A,\mathcal R),

其中：

$\mathcal L$ 是語言；
$\mathcal A$ 是公理與定義；
$\mathcal R$ 是合法推理規則。

若命題 $P$ 存在有限 proof object $\pi$ ，使：

\operatorname{Check}_{\mathcal T}(\pi,P)=\mathrm{true},

則稱 $P$ 在 $\mathcal T$ 中達成 Theorem Closure。

可寫成：

\operatorname{TC}_{\mathcal T}(P)=1.

這正是 Lean、Coq、Isabelle 類系統最核心、也最可靠的能力。

重要的是，Theorem Closure 所要求的通常只是一個有限 proof representation。

例如數學歸納法可以證明：

\forall n\in\mathbb N,\;P(n),

但 kernel 並不需要逐一執行：

P(0),P(1),P(2),P(3),\ldots

直到某個「無限終點」。

它只需要驗證有限規則：

P(0)

以及：

\forall n,\quad P(n)\Rightarrow P(n+1).

因此：

\text{finite proof term} \Rightarrow \text{statement over infinitely many instances}.

這完全是形式數學的正常能力。

問題在於：如果研究者真正關心的是「那些 instance 是否構成同一條生成路徑」，那麼這個問題並沒有自動被回答。

3. 第二個區分：Arrow Validity

考慮狀態空間：

\mathcal S.

對任意兩個狀態：

S,S'\in\mathcal S,

我們引入箭頭：

S\xrightarrow{\alpha}S'.

普通存在性證明可能只要求：

\forall n,\quad \exists S_{n+1}\;P(S_n,S_{n+1}).

但如果研究問題具有過程語義，我們需要更強的要求：

\operatorname{Admissible}(S_n,S_{n+1},\alpha_n).

這表示： $S_{n+1}$ 不是任意滿足某些條件的 witness，而是可以由 $S_n$ 經過被允許的 transition $\alpha_n$ 生成。

因此定義：

\operatorname{AV}(S_n,S_{n+1}) = 1

當且僅當存在一個合法箭頭 $\alpha_n$ ，使：

S_n\xrightarrow{\alpha_n}S_{n+1}.

這與：

\exists S_{n+1}\;P(S_{n+1})

具有本質差異。

後者只回答「下一個狀態存在」。

前者回答：

為什麼它是這一個狀態的下一步？

4. Same-Parent Path：存在很多節點，不代表存在一條路徑

令：

L_n

表示第 $n$ 層所有合法狀態集合。

假設：

L_n\neq\varnothing

對所有 $n$ 成立。

這並不自動推出存在：

(S_0,S_1,S_2,\ldots)

使：

S_n\in L_n

且：

S_n\to S_{n+1}

對每個 $n$ 都成立。

也就是：

\forall n,\quad L_n\neq\varnothing

不等價於：

\exists (S_n)_{n\in\mathbb N}, \quad \forall n,\; S_n\in L_n \land S_n\to S_{n+1}.

差異就在 compatibility。

我們稱後者為 Same-Parent Path Condition。

形式上：

\operatorname{SPP}((S_n)) := \forall n,\; \operatorname{ParentCompatible}(S_n,S_{n+1}).

因此：

\boxed{ \text{State existence} \neq \text{Path existence} }

進一步：

\boxed{ \text{Path existence} \neq \text{Path generation} }

因為即使 classical choice 幫助我們選出一條序列，也不表示存在可執行的生成規則：

S_{n+1}=F(S_n).

5. 第三個區分：Trace Validity

一個真正的過程不只是節點集合，而是 trace：

\tau:\mathbb N\to\mathcal S.

定義：

\tau(0)=S_0

以及：

\forall n,\quad \operatorname{Step}(\tau(n),\tau(n+1)).

若以上成立，稱 $\tau$ 是合法 trace。

也就是：

\operatorname{TV}(\tau)=1.

因此一個過程性 theorem 若只證：

\forall n,\quad \exists S_n\;P_n(S_n),

它還沒有證：

\exists\tau:\mathbb N\to\mathcal S, \quad \operatorname{TV}(\tau)=1.

這裡可看見一個常見語義壓縮：

\forall n\exists S_n

在形式邏輯中可以藉由選擇原理得到一個 total function。

但：

\exists\tau

仍不等於：

\tau(n+1)

是由：

\tau(n)

內生產生。

因此本文區分：

\text{Choice Trace}

與：

\text{Generated Trace}.

6. 第四個區分：Process Completeness

我們現在可以提出初步定義。

對一個宣稱描述過程的證明 $\Pi$ ，若其結論依賴狀態鏈：

S_0,S_1,\ldots

則稱 $\Pi$ 具有 Process Completeness，至少需要：

\mathrm{PC}_1: \quad S_0\text{ 被合法初始化};

\mathrm{PC}_2: \quad \forall n,\; S_n\to S_{n+1} \text{ 的箭頭合法};

\mathrm{PC}_3: \quad (S_n) \text{ 為 same-parent trace};

\mathrm{PC}_4: \quad \text{若使用極限 }S_*,\text{ 必須證明 }S_* \text{ 來自該 trace 的合法 completion};

\mathrm{PC}_5: \quad 任何在極限處使用的性質轉移皆有明確 transfer theorem。

因此：

\operatorname{PC}(\Pi)=1

需要的不只是 theorem conclusion，而是 proof graph 中所有關鍵生成箭頭都有語義閉合。

7. Completion Operator：最容易被忽略的額外箭頭

假設我們已有：

S_0,S_1,S_2,\ldots

接著證明突然定義：

S_*:=\mathcal C(\{S_n\}_{n\in\mathbb N}),

其中 $\mathcal C$ 可能是：

極限；
對角化；
Borel realization；
completion；
compactness extraction；
weak limit；
subsequence selection；
classical choice；
gluing；
extension theorem。

這時證明圖實際上不是：

S_0\to S_1\to S_2\to\cdots\to S_*.

而是：

\{S_n\}_{n\in\mathbb N} \xrightarrow{\mathcal C} S_*.

因此 $\mathcal C$ 是一個新的 proof-level operator。

它必須獨立接受審計。

我們定義：

\operatorname{CO}(\mathcal C)

為 Completion Operator。

核心問題包括：

\operatorname{Domain}(\mathcal C)?

\operatorname{Compatibility}(\mathcal C)?

\operatorname{Preservation}(\mathcal C)?

\operatorname{Uniqueness}(\mathcal C)?

\operatorname{Computability}(\mathcal C)?

以及最關鍵的：

\boxed{ \mathcal C(\{S_n\}) \text{ 是否仍屬於原過程的語義？} }

一個 completion operator 可以在古典分析中完全合法，但仍不是原生成機制的一步。

這正是：

\boxed{ \text{Logical completion} \neq \text{process continuation} }

8. 第五個區分：Computational Realizability

即使：

\exists\tau:\mathbb N\to\mathcal S

且：

\operatorname{TV}(\tau)=1,

仍然不代表 $\tau$ 可計算。

若我們希望過程真正具有演算法意義，需要存在：

F:\mathcal S\to\mathcal S

使：

\tau(n+1)=F(\tau(n)).

並且 $F$ 在有限資源下可求值。

因此我們引入：

\operatorname{CR}(F)=1

表示 $F$ 具 Computational Realizability。

更進一步，如果存在極限：

\tau(n)\to S_*,

若要把「接近極限」轉成可操作計算，通常還需要 modulus：

\mu:\mathbb Q_{>0}\to\mathbb N,

使：

n\ge\mu(\varepsilon) \Rightarrow d(\tau(n),S_*)<\varepsilon.

若 $\mu$ 可計算，極限才具有更強的 constructive content。

因此：

\text{existence} \neq \text{effective existence}.

9. 五層證明審計框架

本文提出以下五層框架。

Layer 1 — Kernel Validity

問題：

\Gamma\vdash T?

檢查 proof term 是否能由可信 kernel 通過。

Layer 2 — Specification Validity

問題：

T \stackrel{?}{=} \text{真正想回答的問題}.

這一層防止：

\text{proof correct} + \text{problem encoded too weakly}.

Layer 3 — Arrow Validity

問題：

S_n\to S_{n+1}

是否具有合法 process semantics。

不能只證：

\exists S_{n+1}.

Layer 4 — Trace Validity

問題：

\exists\tau

是否真的是 same-parent path。

若：

\tau(n)

與：

\tau(n+1)

只是分別被選出，則仍需要 compatibility proof。

Layer 5 — Computational Realizability

問題：

\tau

或：

\operatorname{Step}

是否可以被演算法實現。

這一層不一定是所有數學 theorem 的必要條件，但對宣稱「過程」「生成」「演化」「模擬」的 theorem 特別重要。

10. 一個最小反例模式

考慮：

\forall n\in\mathbb N, \quad \exists x_n\in X_n.

形式上，每一層都有 witness。

現在加入：

R_n\subseteq X_n\times X_{n+1}.

若 theorem 需要的是：

\exists (x_n), \quad \forall n,\; (x_n,x_{n+1})\in R_n,

那麼：

\forall n,\quad X_n\neq\varnothing

顯然不夠。

甚至：

\forall n,\forall x_n\in X_n, \quad \exists x_{n+1}\in X_{n+1}, \quad (x_n,x_{n+1})\in R_n

雖然能在 choice 下構造 path，仍不一定給出 computable transition。

因此至少存在三種強度：

E_1: \quad \forall n\exists x_n,

E_2: \quad \exists (x_n)\forall n\;R_n(x_n,x_{n+1}),

E_3: \quad \exists F\; \forall n,\; x_{n+1}=F(x_n).

通常：

E_3\Rightarrow E_2\Rightarrow E_1,

但反方向不自動成立。

11. 「如果，所以，然後」真正的問題是什麼？

數學證明本來就必須包含大量：

P\Rightarrow Q.

所以「如果、所以、然後」本身完全不是缺陷。

真正需要審計的是：

每一個 implication 是否仍位於同一個問題域與同一個生成語義中？

若：

P_n\Rightarrow P_{n+1}

是合法 successor theorem，則沒有問題。

若某一步突然變成：

\{P_n\}_{n\in\mathbb N} \Rightarrow Q

並且 $Q$ 透過一個新的 $\mathcal C$ 被實現，那麼必須標記：

\boxed{ \text{這不是普通 successor arrow，而是 completion arrow。} }

形式證明系統可能會把兩者都表示成 function application。

但研究語義不能因此把它們視為同一種步驟。

12. Proof Assistant 的能力邊界不是「不夠嚴格」，而是「只驗你寫進去的規格」

這裡需要避免一個常見誤解。

如果 Lean 通過了一個 theorem，但 theorem 並未要求 process completeness，不能說 Lean「漏掉」了 process completeness。

Lean 的工作是：

\operatorname{Check}(\text{formal specification}).

不是：

\operatorname{Infer}(\text{all unstated scientific obligations}).

因此真正的問題是：

\boxed{ \text{omitted semantic obligation} }

沒有被寫入 formal statement。

Proof assistant 無法驗證一個從未被形式化的 requirement。

所以未來形式化數學若要處理 process-sensitive theorem，必須把：

\operatorname{Step}, \quad \operatorname{Trace}, \quad \operatorname{ParentCompatibility}, \quad \operatorname{CompletionOperator}, \quad \operatorname{TransferLaw}

升格為一級形式物件。

13. AI 數學時代的新風險

當 AI theorem prover 越來越強，可能出現一個反直覺現象：

\text{formal closure capability}\uparrow

不一定自動推出：

\text{problem ontology judgment}\uparrow.

AI 可能非常擅長：

\text{找到一條能封閉 theorem 的路}

卻不一定主動追問：

\text{這條 theorem 是否就是最值得證明的問題？}

因此可能出現：

\boxed{ \text{specification-minimal resolution} }

亦即：

在形式規格允許的範圍內，找到最容易被完整證明的合法路徑。

這不是錯。

但它可能比研究者原本口語上理解的「解掉整個問題」更窄。

因此未來 AI 數學系統不能只評估：

\text{proof success rate}.

還應評估：

\text{semantic depth},

\text{arrow completeness},

\text{problem reconstruction ability},

與：

\text{claim scope discipline}.

14. Process-Complete Theorem 的初步規格

本文提出一個初步 schema。

對任意動態 theorem：

\mathfrak P = (S_0,\mathcal T,\mathcal I,\mathcal G),

其中：

$S_0$ ：初始狀態；
$\mathcal T$ ：合法 transition relation；
$\mathcal I$ ：需要維持的 invariants；
$\mathcal G$ ：目標性質。

一個 process-complete proof 至少應證明：

\exists\tau,

使：

\tau(0)=S_0,

\forall n,\quad \mathcal T(\tau(n),\tau(n+1)),

\forall n,\quad \mathcal I(\tau(n)),

並且若：

\tau\to S_*,

則必須證：

\operatorname{LegalCompletion}(\tau,S_*),

以及：

\mathcal G(S_*).

若 theorem 宣稱演算法性，則再要求：

\tau(n+1)=F(\tau(n))

其中 $F$ 為可計算 transition。

因此：

\boxed{ \text{Process-Complete Proof} = \text{Theorem Closure} + \text{Arrow Closure} + \text{Trace Closure} + \text{Completion Closure} }

在需要計算意義時，再加：

+ \text{Computational Closure}.

15. 核心命題

本文的核心命題可濃縮為四句。

第一：

\boxed{ \text{A proof of existence is not automatically a proof of generation.} }

第二：

\boxed{ \text{A family of valid finite stages is not automatically a completed path.} }

第三：

\boxed{ \text{A legal completion operator is not automatically the next step of the original process.} }

第四：

\boxed{ \text{Machine-checked theoremhood does not by itself establish process completeness.} }

這四句不否定形式化數學。

相反，它們要求更強的形式化。

16. 結論

形式化證明的成功，解決了數學史上一個極為重要的問題：我們終於可以把大量 proof checking 從人類信任轉移到機器 kernel。

但下一個問題已經出現：

當 theorem 本身描述一個過程時，我們究竟證明了命題，還是證明了過程？

如果 proof 只說：

\forall n\exists x_n,

而研究問題實際需要：

x_0\to x_1\to x_2\to\cdots,

則兩者之間仍存在語義距離。

如果 finite corrections 最後透過新的 diagonal operator 被組成一個 smooth object，那麼我們必須區分：

\text{realization}

與：

\text{trajectory completion}.

如果 classical choice 產生一個 total function，則我們必須區分：

\text{selected object}

與：

\text{generated object}.

因此，未來高階形式數學與 AI theorem proving 的重要方向，不只是建立更多可驗證 theorem，而是建立：

\boxed{ \text{Proof Systems That Can Audit Their Own Arrows.} }

也就是：不只問結論是否成立，還要問每一個「所以」究竟代表哪一種合法轉換。

17. 系列後續

本文只建立一般理論框架。

下一篇將集中處理：

Paper 02 — 下一步到底為什麼是下一步：Arrow Legitimacy 與 Same-Parent Path

核心問題是：

\boxed{ \text{What makes the next state genuinely the next state?} }

並進一步建立 successor legality、parent compatibility、branch consistency 與 path preservation 的形式模型。