《形式化打開歷史帳本——數學證據分層、隱性假設與證明債務》

《AI 時代數學傳承工程論》08

作者： Neo.K
機構： EveMissLab／一言諾科技有限公司
日期： 2026-10-07（整理日期；原稿未標註日期）
版本： 原稿未標註（本次整理版）

摘要

形式化數學常被視為提升可靠性、可驗證性與可重現性的自然方向。隨著 AI 降低 theorem formalization、proof search、dependency tracing 與 machine checking 的成本，更多數學成果將被轉換為可執行、可檢查與可追蹤的形式。然而，形式化不只會「增加證據」，也會暴露大量原本被數學共同體默認吸收的歷史結構：未明寫的 assumptions、folklore lemma、跨論文引用缺口、定義版本漂移、依賴邊界不清、計算環境差異，以及「大家都知道」但未真正被記錄的局部知識。

本文將這些現象統稱為「證明債務」（Proof Debt）與「數學歷史債務」（Mathematical Historical Debt）。本文主張：AI 時代的形式化革命，本質上也是一次大規模的知識帳務重建。它不只告訴我們哪些 theorem 能被機器接受，更迫使數學文明回答：某個 claim 到底依賴哪些前提、哪些部分是證明、哪些部分是重建、哪些部分仍只是共同體習慣。

本文提出數學證據分層模型、顯式債務／隱式債務區分、債務暴露率、債務償還優先級與「局部 closure 不等於全域 closure」等概念，並指出一個重要風險：若形式化被誤解為「所有歷史債務都必須立即歸零」，數學可能走向 Proof-Debt Zeroism，使 AI 原本應降低的驗證成本轉化為新的合規壓力。真正成熟的制度，不是消滅所有債務，而是讓債務可見、可分類、可追蹤、可優先排序，並在風險與價值相稱的情況下逐步償還。

關鍵詞

形式化數學、證明債務、數學歷史債務、AI 驗證、隱性假設、Lean、可重現性、依賴圖、形式證明、知識治理

1. 形式化真正打開的是什麼？

談到 proof assistant、formal verification、machine-checkable mathematics 時，最直覺的理解通常是：

\boxed{ \text{更多形式化} \Rightarrow \text{更多可靠性}. }

這當然成立一部分。

但本文主張，更深的結果其實是：

\boxed{ \text{更多形式化} \Rightarrow \text{更多歷史結構被迫顯式化}. }

也就是：

形式化不只是在驗證今天的新 theorem，它還會把昨天被默認略過的東西重新翻出來。

2. 數學文明一直都依賴「不完全寫出來」

成熟數學共同體之所以能高效運作，

是因為大量資訊不需要每次重寫。

例如：

標準 lemma；
常見 notation；
proof idiom；
known reduction；
folklore result；
standard regularity assumption；
canonical construction；
tacit boundary condition。

因此專業文本往往使用：

\boxed{ \text{Compression by Shared Background}. }

這不是缺陷。

而是一種必要壓縮。

若每篇論文都從集合論公理開始，

數學研究將無法運作。

3. 共享背景也是一種「隱性資本」

設某領域共同體擁有的隱性背景為：

K_{tacit}.

則一篇論文真正的可理解內容不是只有：

K_{explicit},

而是：

\boxed{ K_{effective} = K_{explicit} + K_{tacit}. }

對熟悉領域的人：

K_{tacit}\gg0.

因此論文可以很短。

對外部者：

K_{tacit}\approx0,

同一篇論文就突然變得極難進入。

形式化會逼迫：

K_{tacit} \rightarrow K_{explicit}.

4. 這就是形式化的帳本效應

本文稱：

Formalization Ledger Effect

其核心為：

\boxed{ \text{Tacit Dependency} \rightarrow \text{Explicit Dependency}. }

形式系統會問：

這個 theorem 用了哪個 definition？
那個 lemma 從哪裡來？
這個 coercion 合法嗎？
universe level 是什麼？
需要 classical choice 嗎？
這個 result 的 domain 到底是什麼？
這一步依賴哪個 imported theorem？

人類專家可能一眼略過，

kernel 不會。

5. 證明債務

本文定義：

Proof Debt

記為：

D_P.

它指：

某個數學成果在現行知識實踐中可被使用與接受，但其完整 dependency、assumption、formal object 或重建步驟尚未全部顯式化。

可粗略寫成：

D_P(M) = D_A + D_L + D_R + D_F + D_C,

其中：

$D_A$ ：assumption debt；
$D_L$ ：lemma debt；
$D_R$ ：reference debt；
$D_F$ ：formalization debt；
$D_C$ ：computational/environment debt。

6. 證明債務不等於錯誤

這一點非常重要。

若：

D_P(M)>0,

不代表：

M=\text{false}.

它可能只代表：

數學共同體依賴共享背景，沒有把所有東西重新展開。

因此：

\boxed{ \text{Unformalized} \neq \text{Wrong}. }

以及：

\boxed{ \text{Implicit} \neq \text{Invalid}. }

否則形式化制度很容易把：

尚未被機器展開

誤判成：

可疑數學。

7. 數學歷史債務

Proof Debt 是局部成果層。

更大的概念是：

Mathematical Historical Debt

記為：

D_H.

它包括跨世代累積的：

folklore；
legacy notation；
lost proofs；
inaccessible sources；
citation chains；
incompatible definitions；
obsolete computational environments；
assumptions inherited without reinspection。

因此：

\boxed{ D_H = \sum_t D_P^{(t)} + D_{\text{institutional}} + D_{\text{archival}}. }

形式化越深入，

這些東西越容易被重新看見。

8. AI 會讓「債務暴露率」快速上升

過去人工 formalization 很昂貴。

因此人類不會：

為了每個 theorem 去追完整 dependency closure。

但 AI 改變：

C_F = \text{Formalization Cost}.

若：

C_F\downarrow,

則更多數學會進入形式化流程。

因此：

\boxed{ E_D = \text{Debt Exposure Rate} \uparrow. }

也就是：

我們不是突然有更多債務，而是突然看見以前沒被統計的債務。

9. 可見債務與實際債務

設：

D_{visible}(t)

為可見債務，

D_{actual}(t)

為實際存在的債務。

AI 時代常可能出現：

D_{visible}\uparrow

但：

D_{actual}

未必增加。

因此：

\boxed{ \text{More Detected Debt} \neq \text{More Broken Mathematics}. }

這是一個很重要的解讀原則。

10. 隱性 assumptions 是最常見的債務之一

設自然語言 claim 為：

C.

真正可證明的形式可能是：

A_1\land A_2\land A_3\Rightarrow C.

但論文中可能只寫：

C.

因為：

A_1,A_2,A_3

在領域裡被視為標準背景。

形式化後：

\boxed{ \text{Hidden Assumption} \rightarrow \text{Explicit Obligation}. }

這本身是好事。

但也會增加 perceived burden。

11. Folklore Debt

很多數學領域都有：

大家都知道這個 lemma。

但：

沒有正式 citation；
citation 很舊；
proof 分散；
版本不一致。

這可以稱為：

D_{folk}.

形式化系統會逼迫問：

到底哪一版？

這使：

\boxed{ \text{Folklore} \rightarrow \text{Tracked Dependency}. }

12. Citation Debt

有些論文引用：

A\rightarrow B\rightarrow C\rightarrow D.

但實際上：

B 引錯頁；
C 用的是不同假設；
D 的 lemma 只對特例成立。

人類共同體可能透過默契修補。

機器重建時就會暴露：

Citation Debt

D_{cite}.

這不是單純 bibliographic error。

它可能影響：

\text{Dependency Integrity}.

13. Definition Drift

同一個概念在不同年代可能有：

Def^{(1)}, Def^{(2)}, Def^{(3)}.

而論文 A 使用：

Def^{(1)},

論文 B 默認：

Def^{(2)}.

形式化整合時會出現：

\boxed{ Def^{(1)}\not\equiv Def^{(2)}. }

這形成：

Definition Drift Debt

14. Scope Debt

有些 proof 在局部環境成立，

但後來被引用時 scope 被放大。

例如：

M|_{\Omega}

後來被默認成：

M|\text{all domains}.

這類問題可稱：

D_{scope}.

形式化會逼迫 domain 被顯式指定。

因此：

\boxed{ \text{Scope is part of proof}. }

15. Computational Debt

對 computer-assisted mathematics 而言，

除了 theorem 本身，

還有：

compiler；
library；
numerical precision；
random seed；
hardware assumption；
data format；
dependency version。

因此：

D_{comp}

可能在多年後使結果：

理論上可重現，

但實際上已無法執行。

這就是：

Computational Historical Debt

16. Formalization Debt

某些成果即使完全可信，

仍可能沒有對應：

Lean proof；
Coq proof；
Isabelle proof；
machine-readable theorem。

這種狀態本身不等於缺陷。

但若某領域未來高度依賴形式 library，

則：

D_F

會影響：

能否被 AI 或 proof assistant 直接重用。

因此 Formalization Debt 具有：

\boxed{ \text{future interoperability cost}. }

17. 數學證據不是單一層

本文提出一個證據分層：

E0：自然語言敘述

\text{Claim}.

E1：自然語言證明

Claim+Proof.

E2：可重現計算

Claim+Proof+Computation.

E3：依賴與來源圖

Claim+Dependency+Provenance.

E4：形式化 statement

\text{FormalClaim}.

E5：kernel-checkable proof

FormalClaim+ProofTerm.

因此：

\boxed{ E_0<E_1<E_2<E_3<E_4<E_5 }

是證據層級，

不是「數學價值排序」。

18. 高證據層不保證高理解

即使：

E_5=1,

也不代表：

HumanUnderstanding=1.

同樣：

E_5=1

也不自動保證：

IntentAlignment=1.

因此：

\boxed{ \text{Evidence Completeness} \neq \text{Semantic Completeness}. }

19. Kernel closure 只是局部 closure

假設某 theorem 在 Lean 裡：

KernelAccepts(P)=1.

可以說：

C_L=1

其中：

C_L = \text{Local Formal Closure}.

但仍可能：

C_S<1,

其中：

C_S = \text{Semantic Closure}.

甚至：

C_G<1,

其中：

C_G = \text{Global Intent Closure}.

因此：

\boxed{ C_L=1 \not\Rightarrow C_G=1. }

20. 形式化會把歷史債務變成新 obligation

一旦某個依賴被發現，

就會自然產生：

那我們是不是也要補它？

形成：

D_P \rightarrow O_P,

其中：

O_P = \text{Proof Obligation}.

當大量歷史債務被揭露時：

\boxed{ E_D\uparrow \Rightarrow O_P\uparrow. }

這就是後續「證書義務膨脹」的入口。

21. 債務發現與債務償還必須分開

一個制度可以做到：

Discover(D_P)=1

但不必：

Repay(D_P)=1

立刻成立。

這是關鍵。

因為：

\boxed{ \text{Visibility} \neq \text{Immediate Obligation}. }

否則形式化工具越好，

制度負擔反而越大。

22. 債務應該分級

本文提出：

Proof Debt Priority Classes

P0：可忽略債務

notation mismatch；
harmless metadata gap。

P1：低風險債務

citation incomplete；
known standard lemma 未形式化。

P2：中風險債務

assumption ambiguity；
dependency version mismatch。

P3：高風險債務

theorem scope 不清；
critical computation 不可重現；
proof gap。

P4：關鍵債務

claim 可能因此不成立；
foundational dependency broken。

因此：

\boxed{ Priority(D) = f( \text{Risk}, \text{Impact}, \text{Centrality}, \text{Reuse}, \text{RepairCost} ). }

23. 中央性很重要

某個小 lemma 如果被：

10^5

個結果依賴，

即使它本身很小，

其：

Centrality\gg0.

因此：

\boxed{ \text{Repair Priority} \not\propto \text{Theorem Fame}. }

反而可能是：

\text{Dependency Centrality}

更重要。

24. AI 可以做數學「債務盤點」

這可能成為未來非常重要的用途。

AI 可以建立：

G_D = \text{Debt Graph}.

節點：

theorem；
definition；
computation；
source；
formal artifact。

邊：

depends on；
cites；
assumes；
reuses；
formalizes。

然後標記：

missing；
stale；
uncertain；
unverified；
incompatible。

25. 從形式證明工具到數學會計系統

因此 proof assistant 的未來用途可能不只是：

驗證 theorem。

還可能是：

\boxed{ \text{Mathematical Accounting Infrastructure}. }

也就是記錄：

我們知道什麼；
依賴什麼；
哪裡還欠；
哪裡已償還；
哪裡只是 provisional。

26. 「所有債務都應該歸零」是一種危險幻覺

當形式化能力變強，

很容易出現：

既然能補，為什麼不全部補？

這就是：

Proof-Debt Zeroism

其隱含目標：

\boxed{ D_P\rightarrow0. }

對有限範圍或高風險領域，

這可能合理。

但對整個數學文明：

D_P=0

幾乎不現實。

27. 為什麼零債務不現實？

因為數學一直在增長：

K(t)\uparrow.

只要新知識產生，

新的：

definitions；
connections；
computational environments；
translations；

也會產生。

因此：

\boxed{ \frac{dD_P}{dt} \neq0. }

甚至：

\frac{dD_P}{dt}>0

可能是健康成長的副作用。

28. 好的數學制度不是零債務，而是可治理債務

更合理目標是：

\boxed{ D_P \text{ is visible, typed, prioritized, and recoverable}. }

也就是：

Governed Debt

而不是：

Zero Debt

29. 形式化的真正價值之一，是讓「不知道」變得可見

一個成熟知識系統不需要假裝：

我們全部都知道。

更好的狀態是：

\boxed{ \text{Known} + \text{Unknown} + \text{Unformalized} + \text{Unreproduced} + \text{Uncertain} }

都被標記。

這就是：

Epistemic Ledger

30. 歷史債務與傳承直接相關

如果某個 theorem：

citation chain 斷裂；
assumptions 模糊；
definition 已漂移；

那麼下一代就更難重新進入。

因此：

\boxed{ D_H\uparrow \Rightarrow ReentryCost\uparrow. }

也就是：

證明債務其實也是傳承債務。

31. 形式化可以降低未來傳承成本

如果重要基礎結構被：

明確定義；
dependency-mapped；
versioned；
formalized；

則未來：

C_{reentry}\downarrow.

因此形式化不是只有：

\text{Verification}.

還具有：

\boxed{ \text{Intergenerational Memory Compression}. }

32. 但形式化不能代替歷史敘事

形式圖可以告訴我們：

A\rightarrow B\rightarrow C.

卻未必告訴：

為什麼當年會想到 B；
哪個障礙促成 C；
哪條失敗路徑最重要。

所以：

\boxed{ \text{Dependency Graph} \neq \text{Historical Understanding}. }

兩者應互補。

33. 債務清理本身也可能產生新知識

有些 hidden assumption 被挖出後，

可能導致：

theorem strengthening；
theorem weakening；
generalization；
counterexample；
new abstraction。

因此：

\boxed{ \text{Debt Repair} \rightarrow \text{Mathematical Discovery}. }

這是形式化非常有價值的一面。

34. AI 會把「修舊帳」變成新研究方向

當 AI 能大量追 dependency，

歷史數學不再只是：

archive。

而可能成為：

\boxed{ \text{active reconstruction frontier}. }

也就是：

哪些經典結果可以被重構？
哪些 proof 可以被壓縮？
哪些 folklore 可以正式化？
哪些 definitions 可以統一？

35. 但不能讓「修帳」吞掉「做數學」

如果整個制度變成：

\text{Researcher} \rightarrow \text{Debt Repair Worker},

則會失去：

exploration；
conjecture；
theory building；
new language generation。

因此：

\boxed{ \text{Debt Governance} \neq \text{Research Substitution}. }

36. 必須有債務預算

可以設：

B_D(M)

為某一成果或領域可合理投入的：

Debt Repair Budget

由：

B_D = f( \text{Risk}, \text{Impact}, \text{Centrality}, \text{FutureReuse}, \text{Cost} )

決定。

若：

MarginalBenefit_{repair} < MarginalCost_{repair},

就應允許：

\boxed{ \text{Stop}. }

37. Stop Condition 是形式化文明的重要能力

一個好的驗證制度不只會問：

還能驗什麼？

還要問：

什麼時候已經足夠？

即：

\boxed{ Stop(M) = 1 }

當：

主要風險已控制；
關鍵 dependency 已確認；
高影響債務已處理；
其餘債務已標記。

38. 從「全域完備幻想」轉向「局部充分閉包」

數學文明不需要：

GlobalClosure=1.

更現實的是：

\boxed{ LocalSufficientClosure(M)=1. }

也就是：

對當前 claim、風險與用途而言，證據已足夠。

這與：

\text{Absolute Completeness}

不同。

39. AI 時代的形式化治理原則

本文提出五項原則：

39.1 顯式優於隱式，但不是所有隱式都必須立即消滅

39.2 債務發現與債務償還分離

39.3 高風險、高中央性優先

39.4 形式 closure 不等於語義 closure

39.5 必須允許合理停止

40. 結論

AI 與形式化工具正在讓數學文明第一次有機會大規模重建自己的證據帳本。

這是一個巨大的進步。

它可以讓我們看見：

hidden assumptions；
folklore；
citation gaps；
scope drift；
definition drift；
computational fragility；
unformalized dependencies。

因此：

\boxed{ \text{Formalization} \rightarrow \text{Debt Visibility}. }

但：

\boxed{ \text{Debt Visibility} \neq \text{Immediate Debt Repayment}. }

如果把兩者混為一談，

就可能從：

\text{Verification Revolution}

滑向：

\text{Compliance Explosion}.

真正成熟的數學文明不是：

所有 theorem 都沒有任何債務。

而是：

\boxed{ \text{我們知道債務在哪裡、} \quad \text{知道它有多危險、} \quad \text{知道什麼值得優先修、} \quad \text{也知道什麼時候可以合理停止。} }

因此，AI 時代的形式化不應被理解為：

\boxed{ \text{Make All Mathematics Fully Formal}. }

更好的目標是：

\boxed{ \text{Make Mathematical Obligations Visible, Typed, Prioritized, and Reconstructable}. }

數學不需要一個沒有任何歷史債務的幻想世界。

它需要的是：

一個知道自己欠了什麼，

知道哪些債該還，

並且不會因為開始記帳，

就把整個文明變成會計部門的世界。