LSI-PSD-02 — 邏輯空間積分：從單次證明搜尋到研究空間覆蓋

Logic-Space Integration: From Single Proof Search to Research-Space Coverage

系列： 邏輯空間積分與證明空間動力學 / Logic-Space Integration and Proof-Space Dynamics
系列代碼： LSI-PSD
論文序號： 02
版本： v2.0 Expanded Edition
日期： 2026-08-17
理論發起： Neo.K
協作整理： Aletheia / GPT-5.6 Sol
文件地位： 方法論核心論文 / Coverage Formalization Paper
Canonical source： UTF-8 Markdown
Canonical math delimiters： $...$ 與 $$...$$

研究地位聲明：本文建立「邏輯空間積分」的操作性數學框架，用來描述長程 AI 數學研究中已探索、已驗證、已排除、已回訪與仍未知的研究區域。本文所稱的 coverage、integration、saturation、basin、obstruction coverage 等量，首先是對特定搜尋制度之可觀測研究狀態的度量，不等於對所有可能證明、所有可能表示、所有可能公理擴張或數學真理本身的完整測度。本文不主張已能計算任何公開未解問題的「真實總證明空間百分比」，更不把 coverage 高、novelty 下降或局部飽和視為原命題錯誤、不可證、不可判定或已被反證的證據。

摘要

當 AI 數學研究從單次輸出擴張到數百、數千甚至更長的持續研究輪次時，「是否找到最終證明」不再足以描述研究系統的進度。大量中間引理、失敗路徑、表示切換、反例候選、形式驗證、數值實驗與跨路線匯流會形成一個具有歷史、局部性與重訪結構的研究空間。若這些資料只以最後成功或失敗二分，則研究系統無法回答一個更基礎的問題：我們究竟探索了什麼，以及新增一輪研究到底增加了多少可審計的新資訊？

本文提出「邏輯空間積分」的第一個完整形式化框架。承接 LSI-PSD-01 所定義的搜尋制度

本文把研究空間區分為形式可證域、制度可達域、觀測域、驗證域與暫存研究記憶，並在適當的語義商空間上定義 coverage function：

由此定義理想化的邏輯空間積分：

以及增量：

但本文特別指出：在真正未解數學問題中，分母 $\bar\Omega_R(Q)$ 通常未知，測度 $\mu$ 也不存在天然唯一選擇。因此， $I_N$ 首先是一個理論極限量，不能被輕率轉譯為「已探索了 $73\%$ 的證明空間」。可操作實驗應改用一組不假裝知道總空間大小的相對量，包括 state coverage、route coverage、obstruction coverage、method-family coverage、representation coverage、verification coverage 與 local-basin coverage。本文因此主張使用 coverage vector：

而不是過早把所有研究歷史壓縮成一個單一百分比。

本文進一步定義負資訊的積分效應：一條經審計的 no-go route 雖然沒有提供最終證明，卻可以合法縮小制度內的候選區域：

其中 $E_N$ 必須有明確條件、適用域與可重現證據。這使「失敗」第一次能被區分為零資訊失敗與正向 coverage gain。本文也定義 marginal research yield：

用來衡量每單位算力、人工審計或生成成本所換得的新增可驗證研究區域。

近年的自動定理證明工作已顯示 proof search 應被視為軌跡與圖搜尋問題。LeanProgress 直接估計 proof trajectory 的剩餘步數；BFS-Prover、AlphaProof、TreeThink 等系統以搜尋樹與 verifier feedback 導航 proof space；Aristotle 將正式 proof search 與非正式推理、lemma generation 結合；AlphaProof Nexus 在公開未解問題上以多代理正式搜尋與 Lean 驗證工作；2026 年的 theorem testing benchmark 則顯示 theorem statement 能成功編譯，不代表其語義已被充分保存，後續 dependent theorems 可提供更強測試。這些結果共同說明，單一 pass/fail 指標不足以表示長程研究進度。

本文最後以 NS-203 長程 Navier--Stokes 語料作為原型案例。該案例已出現 route revisit、cross-series dependency、obstruction confluence 與局部 higher-order sampling，但固定窗口 novelty 統計並不支持「全域 novelty 已崩潰」的結論。這個結果用來示範本文最重要的原則：coverage 可以局部增加，飽和可以局部成立，而全域證明空間仍然保持未知。

關鍵詞： 邏輯空間積分、證明空間覆蓋、proof search、研究空間、coverage vector、局部飽和、negative information、obstruction、route graph、驗證權重、AI 數學研究、Navier--Stokes

1. 從「有沒有證明」轉向「研究空間增加了什麼」

1.1 單次 theorem proving 的成功函數

最簡單的自動定理證明評估可以寫為：

這個成功函數對 benchmark 很有用。

它回答：

這個系統是否找到一個 verifier 接受的證明？

但它刻意忽略：

• 嘗試過多少條路；
• 哪些中間引理已被證明；
• 哪些表示被證明難以處理；
• 哪些方法族反覆撞上同一障礙；
• 哪些失敗其實排除了大區域候選；
• 哪些路徑只是假重複；
• 哪些新結果沒有進入最終 proof term，卻能被其他研究重用。

因此：

是一個終點指標，不是研究歷史指標。

1.2 長程研究需要另一種進度概念

假設 AI 在固定問題 $Q$ 上持續工作 $N$ 輪。

每一輪產生研究事件：

其中可以分別表示：

• $q_i$：當輪局部目標；
• $s_i$：進入時研究狀態；
• $a_i$：採取的方法或 action；
• $r_i$：輸出的候選結果；
• $v_i$：驗證狀態；
• $t_i$：時間、版本或 provenance。

完整歷史為：

如果最後仍沒有證明，傳統成功函數仍然只有：

但這不代表：

反而可能：

因此長程研究需要回答另一個問題：

本文把這個問題稱為：

即「邏輯空間積分」。

2. 邏輯空間不是字串空間

2.1 最粗糙的錯誤：把 token 數當探索量

如果把每一段生成文字都視為一個新研究點，則只要修改：

• 符號名稱；
• 句子順序；
• lemma 名稱；
• Markdown 排版；
• 變數字母；
• 同義詞；
• proof sketch 的自然語言表述；

就可以無限增加「探索量」。

這顯然不合理。

因此：

甚至：

2.2 一階研究單元

本文暫時把一個研究單元表示為：

其中：

• $P$：proposition / subgoal；
• $A$：assumptions；
• $M$：method / transformation；
• $R$：result；
• $O$：obstruction / failure mode；
• $V$：verification status。

兩段文字若表面不同，但經 canonicalization 後得到相同：

則應視為同一或高度等價研究狀態。

2.3 語義等價關係

定義暫定等價關係：

若 $x,y$ 在研究任務所關心的結構上不可區分。

例如：

真正要積分的空間不應是 $\Omega$，而至少是：

這裡的 $\sim$ 不可能一次完美定義。

因此 LSI-PSD-03 將專門處理：

問題。

本文先使用「任務相對等價」作為操作性前提。

3. 搜尋制度與五種不同的空間

3.1 搜尋制度回顧

承接第一篇，定義搜尋制度：

其中：

• $\mathcal A$：公理與背景理論；
• $\mathcal L$：表示語言；
• $\mathcal M$：方法族；
• $\mathcal V$：驗證系統；
• $B$：資源界；
• $\mathcal K$：既有知識與資料；
• $\Sigma$：調度、搜索與 agent 策略。

同一個 $Q$ 在不同 $R$ 下，具有完全不同的可達區域。

所以：

不是數學宇宙本身。

它只是：

在目前制度下，可被產生、表示、調用、驗證或探索的研究狀態集合。

3.2 形式可證空間

令：

表示在背景形式系統 $\mathcal A$ 中與 $Q$ 有關的合法 proof states、proof objects 與中間命題空間。

這已經可能極大，甚至根本不可實際枚舉。

3.3 制度可達空間

加入語言、方法、工具與資源限制：

它表示：

理論上此搜尋制度有機會走到的區域。

這個集合仍然通常未知。

3.4 實際觀測空間

經過 $N$ 輪後真正走過：

這是我們最容易從 logs、artifact、proof state、tool execution 與版本紀錄重建的部分。

3.5 已驗證空間

只有通過指定驗證門檻的部分進入：

可再分級：

但不同級別不可混稱為相同強度。

3.6 研究記憶空間

研究系統還可能保存：

其中包含：

• 未完成 proof sketch；
• speculative conjecture；
• failed branch；
• counterexample candidate；
• heuristic；
• literature lead；
• unresolved obstruction。

所以：

但：

仍然可能具有高 routing value。

3.7 五空間不能混在一起

因此至少要維持：

五者分離。

尤其不能從：

就推成：

更不能推成：

4. 邏輯空間積分的理想定義

4.1 coverage function

在語義商空間：

上，定義 coverage function：

直觀上：

表示尚未觀察；

表示在指定研究標準下已充分探索；

中間值表示：

• 僅生成；
• 僅局部驗證；
• 僅一種表示採樣；
• 缺乏獨立重現；
• 仍有重要子路徑未處理。

4.2 理想積分

若 $\bar\Omega_R(Q)$ 上存在適當測度 $\mu$，定義：

這是本文名稱「邏輯空間積分」最直接的形式。

如果：

則形式上：

但這個 normalization 只在 $\mu$ 已被合理定義時有意義。

4.3 為什麼不能隨便說「已探索 80%」

對真正困難數學問題，我們通常不知道：

甚至不知道：

更不知道不同 proof state 是否應該等權。

例如：

一千個同類參數變體：

可能比不上一次表示變換：

所帶來的新研究區域。

因此：

4.4 不完整測度仍然有用

即使無法得到全域 $\mu$，仍可在局部 chart：

上定義：

這意味著：

全域 coverage 不可知，不妨礙局部 coverage 可測。

這一點對後續「局部飽和」至關重要。

5. 從單一積分改成 Coverage Vector

5.1 為什麼單一 scalar 太粗

假設兩個研究系統：

系統 A：

• 嘗試很多 states；
• 幾乎沒有驗證；
• route 很重複。

系統 B：

• states 較少；
• route 多樣；
• 每條都高度驗證；
• obstruction catalog 完整。

如果都壓成一個 $I_N$，可能失去最重要差別。

因此本文定義 coverage vector：

5.2 State Coverage

衡量已到訪 canonical research state 的範圍。

操作代理量可寫成：

其中 $V_N^{uniq}$ 是 canonicalized node set。

注意：

是絕對數，不是假裝知道全域分母的比例。

5.3 Route Coverage

令 proof-route graph：

route coverage 可觀察：

或考慮 route family：

其中：

表示兩條路在 transformation skeleton 上等價。

則：

5.4 Obstruction Coverage

定義 canonical obstruction set：

每個 $O_i$ 必須至少包含：

因此：

更重要的是重訪 multiplicity：

以及跨方法匯流度：

5.5 Method-Family Coverage

若方法族為：

定義：

但必須區分「叫了方法名稱」和「真的執行到能產生判定資訊」。

所以引入 method engagement weight：

則：

5.6 Representation Coverage

表示空間可能包含：

例如同一問題可能使用：

• physical variables；
• vorticity form；
• Fourier representation；
• geometric formulation；
• weak formulation；
• functional-analytic representation；
• formal proof assistant encoding。

定義：

衡量真正被採樣的 representation family。

這裡非常重要，因為：

不代表：

5.7 Verification Coverage

定義驗證權重：

例如可以建立分級：

這不是宣稱形式驗證涵蓋所有語義問題，而是表示：

在指定 statement 與形式系統內，其 deductive correctness 的驗證強度更高。

可定義：

6. 驗證不是一個 bit：Verification Lattice

6.1 binary verifier 的優點與限制

Lean 等 proof assistant 對已形式化 statement 可以給出非常強的：

但這仍然不能自動回答：

• $Q$ 是否忠實表達原始自然語言命題；
• 定義是否偷換；
• theorem statement 是否過弱；
• formalization 是否漏掉假設；
• 生成的 theorem 是否保留原 repository 的語義接口。

因此：

6.2 2026 theorem testing 的啟示

2026 年的 automated theorem proving testing 工作提出類似 integration testing 的概念：

生成的 theorem 不只要 compile，還要讓依賴它的 successor theorems 繼續成功。

形式化表示為：

仍不足；

還要求：

這提供一個重要方向：

6.3 驗證格

本文建議把驗證寫成 lattice-like state：

其中：

• $v_{syntax}$：語法合法；
• $v_{formal}$：形式 proof checker 通過；
• $v_{semantic}$：statement 與原命題語義對齊；
• $v_{independent}$：獨立方法或獨立 agent 重現；
• $v_{transfer}$：作為上游結果時能否支援下游 theorem / computation。

因此兩個都「verified」的 artifact，仍可能驗證結構不同。

6.4 coverage 必須攜帶驗證資訊

因此：

不應只由「曾到訪」決定。

更合理：

例如一個簡化版本：

其中 $e_{j,N}$ 表示不同證據通道是否覆蓋該狀態。

這個公式不是唯一正確定義，而是說明：

coverage 可以是多證據累積，而不是 visit counter。

7. 增量：研究真正重要的是 $\Delta I$ 而不是輸出長度

7.1 積分增量

定義：

如果第 $N+1$ 輪只是重新描述已知內容：

即使輸出：

相反，如果只增加一個短 lemma，但它開啟全新 route family：

即使文字非常短。

因此：

7.2 研究邊際收益

令本輪成本：

定義：

其中 $\widetilde I_N$ 是可操作代理積分。

$\eta_N$ 可稱：

即「邊際研究收益」。

7.3 高產出不等於高收益

可能：

但：

這就是長程 AI 研究最容易出現的假繁榮：

生成量很大，但新 canonical state 幾乎沒有增加。

因此監控系統不能只報：

• paper count；
• token count；
• branch count。

而要報：

8. 負結果如何增加 coverage

8.1 一般直覺：失敗等於沒有進展

在只看最終 proof 的評估中：

但長程研究不應如此粗糙。

8.2 可審計 no-go region

假設某 route family $R_a$ 在條件：

下被嚴格證明無法完成某 closure。

則可定義排除區域：

如果 $E_a$ 有清楚適用域，就可以更新 survivor space：

這是：

8.3 什麼失敗不能算 coverage gain

以下通常不能直接算：

• 模型說「我想不到」；
• 某次 generation timeout；
• syntax error；
• prompt 沒寫清楚；
• 沒有完整跑完搜索；
• 只測了一個參數點；
• 沒有排除等價繞路；
• obstruction 沒有被重現。

這些最多是：

不是：

8.4 負結果分級

可定義：

coverage weight 應隨級別增加，但仍只在其適用域內成立。

9. 路由圖：邏輯空間積分的離散骨架

9.1 proof-route graph

定義：

其中 node 可包括：

edge 可包括：

9.2 Hyperedge 比普通 edge 更自然

很多 proof step 不是：

而是：

因此更一般地應使用 hypergraph：

其中：

9.3 路徑不是證明

一條 graph path：

只表示研究路由。

只有當：

• 所有 required premise 合法；
• inference verified；
• statement fidelity 已確認；
• terminal node 等於 target；

才可稱為正式 proof path。

所以：

9.4 Graph coverage

可以定義局部：

前提是 $U$ 為有限已知 benchmark subgraph。

對未知開放研究空間，則只報：

10. 局部盆地與局部積分

10.1 proof basin

定義一個研究盆地：

若其內部 states 在：

• 方法；
• representation；
• obstruction；
• dependency；
• proof skeleton；

上具有高內部耦合。

10.2 basin coverage

若 $B_i$ 已有有限 canonical map：

若 $|B_i|$ 仍未知，可以用：

10.3 局部飽和不等於全域飽和

可能存在：

但是：

所以：

這是本文與後續第五篇的核心橋樑。

10.4 Representation escape

如果：

已高度飽和，新的表示 $L_2$ 可能建立：

並使：

因此 saturation detector 應輸出：

Current basin under current representation saturated.

而不是：

Problem saturated.

11. Novelty 不是 Coverage，但可以作為增量訊號

11.1 textual novelty 的危險

文本向量距離：

只能反映表述差異。

不能直接當：

11.2 semantic route novelty

更合理：

其中 $W_N$ 是固定大小的回看窗。

固定窗口非常重要。

如果使用全部歷史：

則隨著 $N$ 增加，可比較樣本天然變多，最大相似度會機械性上升。

這會產生假 saturation。

11.3 fixed-window estimator

令窗口：

定義：

再和 random permutation baseline 比較。

11.4 novelty decay 的弱結論

如果：

只能先說：

在目前 representation 與 similarity metric 下，新 artifact 與最近歷史越來越相似。

不能直接說：

更不能說：

12. 邏輯空間積分的多階結構

12.1 一階積分

一階採樣 states：

積分：

12.2 二階積分

採樣 transitions / proof moves：

12.3 三階積分

研究 route relations：

例如：

或：

定義：

12.4 X 階

一般：

因此完整研究狀態不是單一 $I_N$，而是：

這為第四篇「高階證明空間採樣」預留正式接口。

13. Search Progress 與 Coverage：從 LeanProgress 到全域研究歷史

13.1 proof progress 的局部形式

LeanProgress 類工作把 theorem proving 視為狀態轉移：

並估計：

這是一種：

而不是只預測下一 tactic。

13.2 進度不等於覆蓋

但是：

和：

回答不同問題。

$\hat d$ 問：

這條 route 距離 closure 還多遠？

$I_N$ 問：

整個研究制度已經走過哪些區域？

因此：

13.3 二者應聯合

可以建立狀態：

這比單一 success probability 更適合長程研究管理。

14. Tree Search 文獻與「積分」觀點

14.1 BFS-Prover

BFS-Prover 把 formal theorem proving 明確視為大型 proof-search tree 的導航問題。

其核心工程事實是：

依賴：

• node expansion；
• search policy；
• preference learning；
• depth encouragement；
• compiler feedback。

這與本文一致：

proof 不是憑空出現，而是 search regime 對 tree / graph 的取樣結果。

14.2 TreeThink

2026 年 TreeThink 更直接把 theorem-proving tree search 模組化，允許比較不同搜索策略。

這說明：

本身就是研究變數。

因此同一模型、同一 verifier、同一 theorem，只改：

就可能得到不同 coverage。

14.3 AlphaProof

AlphaProof 在 Lean formal environment 中結合 reinforcement learning 與 search，最重要的方法論意義之一是：

可以為大規模探索提供可靠回饋。

本文不把這解讀成「搜索越大就一定接近所有真理」，而是：

因為一部分 branch 可以被嚴格標記為：

15. 從競賽證明到研究級 proof search

15.1 Aristotle 的混合路徑

Aristotle 將：

• Lean proof search；
• informal reasoning；
• lemma generation / formalization；
• geometry solver；

放在同一系統中。

這支持一個重要觀點：

可能跨越多種 representation 與 solver。

因此 coverage 系統不能假設所有 node 都是同質 Lean state。

15.2 AlphaProof Nexus 與 open-problem search

2026 年 AlphaProof Nexus 對公開未解問題進行大規模正式 proof search，並使用多 subagents、Lean compiler feedback 與演化式協調。

它直接把：

帶到 research-level problem setting。

此時「沒有證出來」的剩餘 artifacts 就更值得保存。

因為它們可能包括：

• formalized lemmas；
• failed subgoals；
• reusable constructions；
• proof search statistics；
• library dependencies。

15.3 FormalProofBench 與 MA-ProofBench

2026 年的 FormalProofBench、MA-ProofBench 等 benchmark 把 formal proving 推向 advanced undergraduate / graduate mathematics 與 mathematical analysis。

這些工作揭露：

不能直接外推成：

特別是在分析領域，長依賴鏈、Mathlib 熟悉度、statement formalization 與 remaining subgoal discharge 都可能成為獨立瓶頸。

所以 coverage 需要 domain-sensitive normalization。

16. Premise Retrieval 本身就是 Coverage Operator

16.1 知識庫不是被動背景

形式證明中，模型能不能找到合適 premise，直接影響：

令 retrieval operator：

不同 retrieval policy：

會改變下一步可達 states。

16.2 LeanSearch 類系統的意義

Global premise retrieval / LeanSearch 類工作顯示，大型 Mathlib 搜索本身是 theorem proving 的核心能力。

因此：

和：

必須分開。

知識存在，不代表 agent 可有效調用。

16.3 可達空間受檢索界面限制

因此：

這比單純把 $\mathcal K$ 視為「模型知道的東西」更精確。

17. Theorem Graph 與 Knowledge Graph：Coverage 的跨證明層

17.1 theorem dependency graph

TheoremGraph 類工作把 formal / informal mathematical objects 連成圖。

對本文而言，可把：

與：

分離。

$G^{knowledge}$ 表示已有 theorem dependency；

$G^{search}$ 表示目前研究歷史。

17.2 兩張圖的交集

定義：

這可以觀察：

• agent 是否只在已知 theorem graph 內移動；
• 是否產生新中介節點；
• 是否重建已知結果；
• 是否開啟新的 dependency bridge。

17.3 新增 theorem 不等於新增知識島

一個新 theorem：

如果只是：

的弱改寫，其 graph contribution 可能很小。

反之，一個短 bridge lemma：

若連接兩個長期分離 components：

其 coverage impact 可能巨大。

因此應考慮：

而不只 theorem count。

18. 自主 theorem discovery 與「搜尋本身生成知識」

18.1 proof search 不一定只服務單一 target

2026 年 self-supervised theorem discovery 類研究顯示，形式 proof search 可以在公理系統中產生可驗證的新 theorem。

這表示：

可能副產生：

其中並非所有 $T_i$ 都是 $Q$ 最終 proof 的必要步驟。

18.2 研究積分的生成版本

因此定義：

並考察：

若能判定 theorem 不只是資料庫重複，就可能形成：

18.3 這和最終 proof 成功可分離

可能：

但：

這是長程 AI 數學研究與單次 benchmark 最大差別之一。

19. NS-203：第一個長程案例的 Coverage 解讀

19.1 語料地位

本文使用一個內部長程 Navier--Stokes 研究 corpus 作原型案例。

在保守排除：

• README；
• CHANGELOG；
• roadmap；
• handoff；
• checkpoint；
• audit；

等非 paper-like artifacts 後，第一輪 observatory 得到：

份 NS paper-like artifacts。

注意：

不是 203 個獨立 theorem。

更不是 203 條互不等價 proof route。

19.2 已建立的離散圖

第一輪 extraction 得到：

條 sequence edges；

條 explicit dependency edges；

條 revisit-similarity edges。

這些數字描述的是：

不是 NS 數學真實證明空間。

19.3 局部 higher-order 訊號

語料中可觀察到：

• obstruction confluence；
• coupled confluence；
• recurrence；
• all-order route escalation；
• second-order residue；
• route feedback。

因此某些 basin 顯示：

式的高階再採樣。

但這首先是 corpus-level classification。

不能直接變成 theorem-level 數學階數。

19.4 固定窗口 novelty 的重要負結果

初始 cumulative nearest-neighbor similarity 看起來像 novelty 下降。

但 cumulative estimator 有天然 bias：

隨歷史池增加容易上升。

改成固定窗口後，第一輪分析並未支持全 corpus 已出現顯著 global novelty collapse。

所以現在最保守結論是：

19.5 這恰好是 coverage framework 的用途

如果只有：

我們只知道「沒有最終 proof」。

加入 coverage 後，可以說：

• 某些 route family 已密集採樣；
• 某些 obstruction 有高 confluence；
• 某些 representation 仍有新增資訊；
• 某些 higher-order relations 開始出現；
• global saturation 未被證成。

這是一個嚴格更豐富、但仍不越權的描述。

20. Coverage 不能回答什麼

20.1 不能判定命題真假

即使：

也不能推出：

20.2 不能判定不可證

不能推出：

因為可能只是：

20.3 不能判定 framing 錯誤

即使所有已知 route 反覆匯流，也可能只是：

• 方法族不足；
• representation 太窄；
• intelligence 不足；
• resource bound 太小；
• proof 極長；
• 關鍵 lemma 尚不存在。

所以：

20.4 不能把 observation denominator 當真實 denominator

若觀測到：

已知 route family 被採樣，最多只能說：

在目前 catalog 中採樣了 $80\%$。

不能說：

採樣了宇宙中 $80\%$ 的可能證明。

21. Relative Coverage：未知分母時真正能報什麼

21.1 catalog-relative coverage

假設當前建立候選 catalog：

可定義：

必須明示：

是動態、可擴張 catalog。

21.2 window-relative coverage

對固定最近窗口：

可計算：

這其實更接近 novelty rate。

21.3 basin-relative coverage

如果某 basin 有有限 decomposition：

可計算：

這種局部 coverage 比全域百分比可信得多。

21.4 benchmark-relative coverage

在明確 benchmark：

中，coverage 可合法寫為：

但 benchmark success 不等於研究空間 coverage。

兩者應分開。

22. Coverage Density 與過度採樣

22.1 density

對局部區域 $U$，定義訪問密度：

如果 $\mu_U$ 未知，可使用 normalized local count。

22.2 oversampling

當：

但：

則 $U$ 可能被過度採樣。

定義 oversampling score：

$O_N(U)$ 高意味：

花很多研究成本，但新資訊很少。

22.3 調度策略

因此 scheduler 可以：

即：

• 降低過度採樣 basin；
• 提高低 coverage representation；
• 啟動 independent verification；
• 尋找新的 method family。

23. Coverage Frontier

23.1 定義 frontier

令已觀測區域：

frontier 可定義為：

它表示：

已知與未知的可操作邊界。

23.2 frontier quality

好的 frontier node 應具有：

• 高可驗證性；
• 高分支潛力；
• 與既有 obstruction 不同；
• 低 representation redundancy；
• 足夠 domain relevance。

可定義 heuristic：

23.3 frontier 比「再寫一篇」更重要

長程 AI 研究若沒有 frontier management，就容易：

因此每輪應輸出：

而不是只輸出最新 artifact。

24. Coverage 與 Compression 的對偶

24.1 探索後必須壓縮

若研究歷史長度：

不可能每次把所有原始文本重新讀一遍。

因此需要 compression：

其中 $\mathcal S_N$ 至少保存：

• canonical claims；
• proof dependencies；
• verified lemmas；
• obstruction IDs；
• unresolved frontiers；
• representation history；
• provenance。

24.2 壓縮不能抹掉差異

如果：

但：

則 coverage estimator 會錯誤低估研究空間。

相反，如果：

卻被保存為完全不同 nodes，則會高估 coverage。

所以：

24.3 可逆 provenance

每個 compressed node 應能回指：

否則不能 audit。

25. 動態積分：研究空間會自己改變

25.1 固定 $\Omega$ 是理想化

真正研究中：

• 新 theorem 出現；
• 新 tool 加入；
• 新 representation 被發明；
• 新 benchmark 被建立；
• 舊 obstruction 被修正；
• 公理背景可能改變。

因此：

是時間依賴的。

25.2 moving domain integral

更一般：

因此：

同時受到：

1. coverage 增加；
2. domain 擴張；
3. measure 重新定義；
4. equivalence relation 更新；

影響。

25.3 coverage 下降不一定退步

如果新 representation 讓 domain 擴張：

即使已知內容不減少，normalized coverage ratio 也可能下降。

這不代表退步。

反而可能代表：

這本身是重要知識。

26. Logic-Space Reynolds Transport 類比

26.1 類比而非物理同一

為了處理 moving domain，可借用 transport theorem 的形式類比。

若：

概念上可拆：

本文不宣稱 proof space 真的是物理流體。

這只是 bookkeeping analogy。

26.2 三種研究增長

可寫：

其中：

• $\Delta I_{explore}$：探索原本已定義區域；
• $\Delta I_{expand}$：發現新區域；
• $\Delta I_{reclassify}$：改進 canonicalization / equivalence 後重估。

這三者應分開報告。

27. Saturation Detector 必須是統計程序，不是感覺

27.1 最低要求

要宣稱某 basin 接近 saturation，至少要看到：

同時：

最好還要：

27.2 不能只用文本相似度

需要至少三組特徵：

更好再加入：

27.3 baseline

必須和：

• random permutation；
• shuffled series order；
• synthetic duplication；
• known non-saturated corpus；

比較。

如果 estimator 對所有長 corpus 都自動顯示下降，則它不能證明 saturation。

27.4 regime-change test

若改變：

之後 novelty 重新上升：

則舊 saturation 更可能是：

28. 邏輯空間積分的最小實驗協議

28.1 輸入

研究系統至少需要：

problem_id
formal_or_informal_statement
axiom_background
representation
method_family
verification_channels
resource_budget
artifact_history

28.2 每輪輸出 schema

run_id
parent_state_ids
claim_ids
assumption_ids
method_ids
representation_id
result_ids
obstruction_ids
verification_state
cost
provenance

28.3 canonicalization

每輪先做：

Normalize symbols
Resolve aliases
Extract claims
Extract dependencies
Map obstruction candidates
Map method family
Compare prior canonical nodes

28.4 更新圖

28.5 計算相對量

至少輸出：

28.6 更新 frontier

然後 scheduler 選擇下一輪：

29. 可執行的 Pseudocode

initialize Graph G
initialize Catalog C
initialize ObstructionRegistry O
initialize Frontier F

for run in research_runs:
    artifact = execute(run)

    parsed = extract(
        claims,
        assumptions,
        methods,
        representations,
        dependencies,
        obstructions,
        verification,
        provenance
    )

    canonical = semantic_normalize(parsed)
    matches = retrieve_equivalent_prior_nodes(canonical, G)

    if matches are high-confidence equivalent:
        update_revisit_edges(G, canonical, matches)
    else:
        add_new_nodes(G, canonical)

    add_dependency_edges(G, canonical)
    add_verification_state(G, canonical)
    update_obstruction_registry(O, canonical)

    metrics = compute(
        new_state_count,
        new_route_count,
        obstruction_gain,
        fixed_window_novelty,
        revisit_rate,
        confluence,
        verification_gain,
        marginal_research_yield
    )

    F = update_frontier(G, O, metrics)
    next_run = scheduler(F, metrics)

這個流程最重要的不是演算法細節，而是資料結構要求：

30. Falsifiable Predictions

本文不是只提出詞彙。

它應該能產生可被反駁的觀察命題。

30.1 P1：固定制度下局部邊際收益可衰減

若 basin $B$ 在固定 $R$ 下長期被重複採樣，則可能觀察：

若始終沒有下降，則「局部飽和」假說受到削弱。

30.2 P2：制度切換可重置 novelty

若飽和主要由表示或方法限制引起，改變：

後應有：

至少在初始窗口成立。

30.3 P3：真正 obstruction 應跨表述重現

若 $O$ 是結構性 obstruction，而非 wording artifact，則在語義等價表示間：

應保有某種：

若完全消失，可能表示原 obstruction 只是 representation artifact。

30.4 P4：verified coverage 比 textual novelty 更穩定

真正累積的已驗證節點：

應比純 textual novelty 對 prompt wording 更不敏感。

如果相反，則 canonicalization 或 verification architecture 有問題。

30.5 P5：高品質負結果應降低 future duplication

當 no-go registry 成熟：

且 scheduler 真的使用它時，應看到：

如果沒有，代表 research memory 沒有真正進入決策閉環。

31. 三種積分不能混淆

31.1 探索積分

表示研究到訪量。

31.2 驗證積分

表示被足夠驗證的研究量。

31.3 排除積分

表示被可靠 no-go 排除的候選區域。

因此：

一個成熟 observatory 應至少同時追蹤三者。

32. Coverage Conservation 不成立

32.1 知識不是固定體積流體

不能假設：

永遠有固定分母。

因為：

會擴張。

32.2 新定義可能增加未知量

當發現新的 structure：

可能同時增加：

與：

這是數學研究常見現象。

因此「知道越多，未知越少」不是單調律。

32.3 更合理的更新

其中：

是新研究開啟的未知空間。

33. Coverage 與「越是真理越可能像廢話」的接口

33.1 本篇暫不證明真理—生成性反轉

後續第七篇將研究：

是否存在非單調關係。

本篇只建立必要的測量語言。

33.2 極端閉合的直觀

若某局部問題被約束到：

則剩餘結論可能表面非常簡單。

但是：

不代表：