LSI-PSD-05 — 局部飽和與全域開放：證明空間的多盆地結構

Local Saturation and Global Openness: A Multi-Basin Structure of Proof Space

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

研究地位聲明：本文提出「證明空間多盆地結構」作為長程 AI 數學研究的操作性模型。本文中的 basin、boundary、escape、conductance、frontier 等詞首先是 proof-space observatory 的研究語言；除非另有嚴格數學構造，不應把它們直接等同於傳統動力系統中的吸引盆、拓撲邊界、勢能井或測地結構。本文不主張目前任何有限 AI corpus 已證明 Navier--Stokes、P/NP 或其他未解問題的完整證明空間局部／全域幾何，更不主張某個局部研究盆地的飽和能推出原命題錯誤、不可證、獨立、無法判定或定義失敗。

摘要

當長程 AI 數學研究持續數百、數千乃至更多輪後，「新資訊是否變少」不再是一個單純的全域問題。研究可能在某一組表示、方法、引理依賴與障礙結構中反覆深化，呈現高度 recurrence、route confluence、higher-order resampling 與 audited yield decline；同一時間，其他表示、其他方法族、其他 premise 組合或其他局部區域仍可能持續產生大量新資訊。若把這兩種現象混在一起，便容易犯下一個關鍵錯誤：

\boxed{ \text{local saturation} \not\Rightarrow \text{global exhaustion}. }

本文在 LSI-PSD-01 至 04 的基礎上，建立「證明空間多盆地結構」的操作性框架。固定研究問題 $Q$ 與搜尋制度 $R$ ，在語義 quotient 後的可觀測證明空間上建立加權圖：

\mathcal G_R(Q) = (V_R,E_R,w_R),

其中節點可為 canonical proof states、route states、obstruction states 或高階 relation states，邊則表示已驗證或已稽核的可達、依賴、轉換、重訪、匯流或再進入關係。對任意候選區域 $B\subseteq V_R$ ，本文以內部 recurrence、邊界流量、局部 novelty、跨界 escape rate 與 order-conditioned audited yield 定義一個操作性 basin。一個 basin 可以被高度探索而近似局部飽和，卻仍然只是整體可觀測研究空間中的一個低傳導、高 recurrence 區域。

本文進一步定義：

\phi(B),

表示 basin conductance；

\rho_k(B;N,W),

表示第 $k$ 階、固定時間窗內的 audited novelty yield；

S_K(B),

表示 $K$ 階局部飽和標記；

\Gamma_{\mathrm{esc}}(B,a),

表示某個 escape action $a$ 離開 basin 後帶來的新增資訊增益；

以及：

\mathfrak F_R(N),

表示在既有 corpus 與制度下仍具有可達性但尚未充分展開的觀測 frontier。

本文的重要限制是：frontier 的存在可以支持「目前觀測制度仍開放」，但 frontier 的不可見不能支持「數學全域已封閉」。 因為真正的證明空間可能超出目前表示語言、方法族、retrieval 系統、verifier、模型能力與計算預算。因此本文區分：

\text{observed local saturation},

\text{regime-bounded global saturation},

與不可從有限研究直接主張的：

\text{mathematical global exhaustion}.

2025--2026 年 formal theorem proving 的發展提供了工程上的相鄰證據。LeanNavigator 將 formal proof exploration 表示成 state-transition graph；LeanProgress 顯示局部 tactic 正確性不等於全局 proof progress；BFS-Prover 透過 length normalization 鼓勵更深路徑探索；FETCH 直接辨識語義重複造成的 over-exploration 與評分波動造成的 under-exploration；FormalEvolve 把固定預算下的 candidate repertoire diversity 與 cross-problem coverage uniformity 視為核心目標；LeanSearch v2 指出單一 premise 的局部檢索與完整定理所需的 global premise set 是不同問題；Goedel-Architect 以全局 blueprint refinement 避免對 dead-end strategy 的遞歸打轉；TreeThink 則顯示同一 formal environment 可以被不同 search policy、evaluator 與 tree strategy 重新探索。這些工作並不證明本文的 basin ontology，但共同顯示：proof search 的局部深度、全局覆蓋、多樣性與可達性必須被分開測量。

本文最後重新分析 NS-203 corpus。既有 v0.1 observatory 在保守分類下得到 203 份 NS paper-like artifacts，其中 $T_1=84$ 、 $T_2=107$ 、 $T_3=10$ 、 $T_X=2$ ；大量 recurrence、no-go 與跨系列 confluence 出現在特定研究支線，但固定窗口 novelty 測試並未支持整個 corpus 的單調全域崩塌。因此，NS-203 目前最合理的解讀不是「Navier--Stokes 證明空間被耗盡」，而是：

\boxed{ \text{some proof basins show higher-order resampling while the corpus remains globally open at the observed level.} }

本文由此提出一個更一般的研究原則：長程 AI 研究的成熟標誌，不是讓同一 basin 變得越來越密，而是能辨識自己何時正在重採樣局部結構、何時需要改變 representation／premise／method family／resource regime，並把每次 basin escape 的成功或失敗保存為下一輪研究資料。

關鍵詞： 局部飽和、全域開放、proof basin、proof-space conductance、frontier、basin escape、route recurrence、confluence、audited novelty、global premise retrieval、proof search、AI 數學研究、Navier--Stokes corpus

1. 問題的提出：為什麼「整體新奇度」是一個危險的單一指標

1.1 長程研究不會均勻覆蓋證明空間

設一個研究系統在固定問題 $Q$ 上持續生成：

g_1,g_2,\ldots,g_N.

如果只看文本數量，最自然的直覺是：

N\uparrow \Rightarrow \text{coverage}\uparrow.

但 LSI-PSD-02 與 03 已指出，這個箭頭至少需要經過兩次修正：

第一，生成 artifact 不等於新增有效研究狀態；

第二，表面不同的 artifact 經語義 quotient 後可能落入同一個等價類。

因此真正的計量對象不是：

N,

而是：

\left| \Omega^{\mathrm{obs}}_R(Q)/\sim \right|.

然而，即使已經做了 quotient，仍有第三個問題：研究採樣通常不是均勻的。

LLM、retriever、verifier、prompt、既有 corpus 與研究者偏好會形成路徑依賴，使系統較容易反覆進入某些區域。

1.2 同一個區域可以很深，但旁邊仍然很空

考慮一個簡化圖：

             B3
            /  \
           /    \
      B1=======B2
      |||       \
      |||        \
   dense core     frontier

假設 $B_1$ 內已經存在大量：

lemma variants；
proof routes；
obstruction IDs；
second-order revisits；
confluence relations；
all-order no-go candidates。

則 $B_1$ 可以非常「密」。

但這個密度不能直接推出：

B_2,\ B_3

也同樣被探索。

更不能推出：

V_R=B_1.

所以長程研究必須回答兩個不同問題：

\text{How saturated is this region?}

與：

\text{How much of the reachable space is this region?}

1.3 研究越成功，越容易被自己的成功困住

一個早期有效的方法族可能帶來大量成果：

M_1 \rightarrow L_1,L_2,\ldots,L_m.

這會形成強烈的內部 reinforcement：

retriever 更常抓回 $M_1$ 的相關 lemma；
prompt 更常引用 $M_1$ 的語言；
evaluator 更熟悉 $M_1$ 的成功模式；
knowledge graph 的高中心度節點越來越偏向 $M_1$ ；
後續模型在 context 中看到更多 $M_1$ 的成功歷史。

於是：

P(\text{return to }B_1)\uparrow.

這個現象並不表示 $B_1$ 是錯的。

恰恰相反，它可能是因為 $B_1$ 曾經非常成功。

問題在於：

\text{successful basin} \neq \text{complete proof space}.

2. 從單一空間改成加權研究圖

2.1 可觀測證明空間

固定：

Q=\text{研究問題},

R=(\mathcal A,\mathcal L,\mathcal M,\mathcal V,\mathcal B,\mathcal H),

其中：

$\mathcal A$ ：公理與背景理論；
$\mathcal L$ ：表示與符號語言；
$\mathcal M$ ：方法族；
$\mathcal V$ ：驗證／稽核制度；
$\mathcal B$ ：算力、時間、token、模型調用等預算；
$\mathcal H$ ：已保存的研究歷史。

本文把在 $R$ 下被實際建構、保留或稽核的研究對象寫成：

\Omega_R^{\mathrm{obs}}(Q).

它不是所有數學上可能證明的集合。

它只是：

\boxed{ \text{under regime }R,\ \text{what the research system has made observable}. }

2.2 語義 quotient 後的節點

依 LSI-PSD-03，先建立語義等價關係：

x\sim y.

例如：

$\alpha$ -renaming；
純記號替換；
同一 lemma skeleton；
同一 normalized hypothesis set；
同一 obstruction under audited equivalence；
經證明可逆的 representation change。

令：

V_R = \Omega_R^{\mathrm{obs}}(Q)/\sim.

此後的 basin 分析原則上作用於 $V_R$ ，不是原始文本。

2.3 邊的型別

建立 typed edge：

e=(u,\tau,v),

其中：

\tau \in \{ \text{derive}, \text{depend}, \text{rewrite}, \text{revisit}, \text{contradict}, \text{converge}, \text{generalize}, \text{specialize}, \text{transfer}, \text{escape} \}.

對每條邊給予權重：

w(e)\ge0.

權重可以綜合：

formal verification；
manual audit；
independent replication；
semantic-equivalence confidence；
chronology confidence；
citation／dependency evidence。

因此：

\mathcal G_R(Q) = (V_R,E_R,w_R).

2.4 不把圖本身當作本體

必須保持：

\boxed{ \mathcal G_R(Q) \neq \Omega^{\mathrm{math}}(Q). }

圖是觀測儀器。

它和氣象雷達、粒子探測器、醫學影像一樣，只是在特定解析度下重建一個可操作結構。

若圖沒有看到某個區域，只能說：

\text{not observed}.

不能說：

\text{does not exist}.

3. 操作性 basin：什麼叫「研究被困在一個局部區域」

3.1 Basin 不應只靠 embedding cluster 定義

如果把相似文本聚類後直接命名為 proof basin，會立刻出現錯誤。

同一個詞：

\text{criticality}

可能出現在完全不同的數學機制。

反過來，真正等價的兩條路可能使用不同詞彙。

因此本文要求 basin 至少同時參考：

\text{semantic similarity},

\text{route connectivity},

\text{obstruction identity},

\text{dependency structure}.

3.2 操作性 basin 定義

對：

B\subseteq V_R,

定義內部邊總重：

W_{\mathrm{in}}(B) = \sum_{u,v\in B} w(u,v).

跨界邊總重：

W_{\mathrm{out}}(B) = \sum_{\substack{u\in B\\v\notin B}} w(u,v).

若：

W_{\mathrm{in}}(B) \gg W_{\mathrm{out}}(B),

而且固定時間窗中研究軌跡反覆回到 $B$ ，則 $B$ 是一個候選 basin。

本文把這稱為：

\boxed{ \text{Operational Proof Basin}. }

3.3 Conductance

借用圖論中的 conductance 形式，但不把它宣稱為 proof-space 的自然測度。

定義節點 volume：

\operatorname{vol}(B) = \sum_{u\in B} \deg_w(u).

則：

\phi(B) = \frac{ W_{\mathrm{out}}(B) }{ \min( \operatorname{vol}(B), \operatorname{vol}(V_R\setminus B) ) }.

直覺上：

\phi(B)\downarrow

表示 basin 內部連結強、外部通道相對少。

但低 $\phi(B)$ 仍可能有三種不同解釋：

真正存在結構性分區；
retriever／prompt 導致的人工作業偏差；
corpus 尚未建立跨區邊。

因此 conductance 是診斷量，不是本體結論。

3.4 Recurrence density

令時間窗：

I_{N,W} = \{N-W+1,\ldots,N\}.

令：

r_t(B) = \mathbf 1[x_t\in B].

定義：

R_W(B) = \frac{1}{W} \sum_{t\in I_{N,W}} r_t(B).

若：

R_W(B)\rightarrow1,

表示近期研究高度集中於 $B$ 。

如果此時 novelty 又下降，才開始形成局部飽和候選。

4. 局部飽和必須是多條件，而不是「最近看起來都一樣」

4.1 單一 novelty 不足

定義局部 novelty：

\nu(B,t).

若：

\nu(B,t)\downarrow,

可能只是：

模型變弱；
prompt 固化；
資源不足；
summarization 損失；
retriever 重複；
quotient 太粗；
真正研究空間局部收斂。

所以：

\nu\downarrow

本身不能定義 saturation。

4.2 第 $k$ 階 audited yield

沿用 LSI-PSD-04，令：

A_k(B;N,W)

是固定窗口內進入 basin $B$ 的第 $k$ 階新 artifact 數。

令：

U_k(B;N,W)

是人工或形式稽核後，仍被判為新的有效等價類數。

定義：

\rho_k(B;N,W) = \frac{ U_k(B;N,W) }{ \max(1,A_k(B;N,W)) }.

當：

\rho_k(B;N,W)\rightarrow0,

表示該階 artifact 增加，但有效新類別很少增加。

4.3 多階局部飽和

對指定 $K$ ：

\mathbf \rho_{0:K}(B) = ( \rho_0(B), \rho_1(B), \ldots, \rho_K(B) ).

本文定義 basin $B$ 在窗口 $(N,W)$ 下的操作性 $K$ 階局部飽和標記：

S_K(B;N,W)=1

當且僅當至少同時滿足：

\rho_k(B;N,W)<\varepsilon_k \qquad \forall k\le K,

R_W(B)>\tau_R,

\phi(B)<\tau_\phi,

且：

A_k(B;N,W)\ge m_k,

以避免「根本沒採樣」被誤判成飽和。

4.4 低產量和飽和是不同的

如果：

A_k(B;N,W)=0,

則：

\rho_k=0

沒有任何意義。

因為這可能只是：

\text{no sampling}.

所以局部飽和必須要求：

\text{sufficient attempt density}.

這是整個方法論最重要的防偽條件之一。

5. 局部飽和非傳播原則

5.1 核心命題

本文提出：

\boxed{ S_K(B)=1 \not\Rightarrow S_K(V_R)=1. }

這稱為：

局部飽和非傳播原則 （Local Saturation Non-Propagation Principle）。

它不是深奧定理。

它是一個對研究語言的約束：只要 $B$ 不是已證明等於整個可觀測空間，就不能把局部判定提升成全域判定。

5.2 更強的防誤推論形式

即使：

S_K(B_i)=1

對多個已知 basin：

B_1,\ldots,B_m

全部成立，仍只能得到：

\text{known-basin saturation}.

不能直接推出：

\text{mathematical global exhaustion}.

因為仍可能有：

B_{m+1}

尚未被表示。

甚至可能有新的表示語言：

\mathcal L'

使原本不可見的區域突然出現。

5.3 Regime-bounded global saturation

若在固定 $R$ 下，研究系統已建立一個 audited cover：

\mathcal C_R = \{B_1,\ldots,B_m,F\},

其中 $F$ 是 frontier pool。

若：

S_K(B_i)=1

對所有 $i$ 成立，且：

F

在足夠多次有意識的 escape intervention 後仍沒有穩定新增 audited class，則可以標記：

\boxed{ \operatorname{Sat}^{R,K}_{\mathrm{global,obs}}=1. }

這個量的名稱中必須保留：

R

與：

\mathrm{obs}.

因為它只代表：

在目前制度與觀測器下，已知可達空間呈現全域操作性飽和。

它仍不代表：

\Omega^{\mathrm{math}}

已耗盡。

6. 全域開放：什麼情況下可以說「還有地方沒走」

6.1 Frontier

令：

\mathfrak F_R(N)

是目前觀測到、具有某種可達證據，但尚未充分展開的節點／候選集合。

候選 frontier 可以來自：

unresolved dependency；
unused premise cluster；
new representation；
unexplored counterexample regime；
cross-domain transfer；
independent model proposal；
human-supplied conjectural bridge；
external theorem library；
failed route 的 alternative branch。

6.2 Frontier 不是「未知的全部」

應明確區分：

\mathfrak F_R(N)

與：

V_R^{\mathrm{unknown}}.

前者是：

\text{known unknowns}.

後者甚至沒有被表示。

因此：

|\mathfrak F_R(N)|=0

不能推出：

V_R^{\mathrm{unknown}}=\varnothing.

6.3 觀測性開放證書

如果存在：

f\in\mathfrak F_R(N)

以及至少一條 auditable transition：

u\in B \longrightarrow f,

且展開 $f$ 後產生：

U_k(f)>0,

則可說：

\boxed{ \operatorname{Open}^{R,K}_{\mathrm{obs}}(N)=1. }

即在目前 regime 下，已直接觀察到 proof-space renewal。

這是一個很強但有限的結論：

我們知道目前還沒飽和。

它不需要知道完整空間有多大。

7. Basin escape：研究不只是繼續走，也要知道何時換區域

7.1 Escape action

定義 escape action：

a \in \mathcal A_{\mathrm{esc}}.

例如：

換 representation；
換座標系；
換 invariant；
換 scale；
換 proof assistant；
換 theorem library；
換 premise retriever；
換模型；
換 prompt policy；
換 method family；
引入反例搜尋；
強制跨域 transfer；
暫時移除高中心度 lemma；
從 final theorem 倒推必要條件；
從失敗 obstruction 反向生成新問題。

7.2 Escape gain

令：

\bar\rho_k^{\mathrm{in}}(B)

是 basin 內近期平均 audited yield。

執行 escape action $a$ 後，在窗口 $W'$ 內得到：

\bar\rho_k^{\mathrm{out}}(B,a).

定義：

\Gamma_{\mathrm{esc},k}(B,a) = \bar\rho_k^{\mathrm{out}}(B,a) - \bar\rho_k^{\mathrm{in}}(B).

若：

\Gamma_{\mathrm{esc},k}>0,

則 escape 至少在第 $k$ 階提高了新增有效資訊率。

7.3 Escape 可以失敗，而且失敗也有資訊

若：

\Gamma_{\mathrm{esc},k}\le0,

不能立刻說新 representation 沒價值。

可能原因包括：

新 representation 尚未學會；
verifier 不支援；
retriever 尚未索引；
translation loss；
budget 太小；
新 basin 本身也飽和；
原 basin 與新 basin 其實 quotient-equivalent。

因此每次 escape 都應保存：

( a, B_{\mathrm{src}}, B_{\mathrm{dst}}, \Delta\rho, \Delta\nu, \Delta\phi, \text{failure trace} ).

這些資料會形成下一階 proof-space science 的 corpus。

8. 多盆地結構：證明空間更像 cover，而不是單一區塊

8.1 不要求 basin 互斥

真實研究中：

B_i\cap B_j \neq \varnothing

是常態。

例如：

compactness route；
recurrence route；
energy route；

可能共享：

\text{critical scaling}.

所以本文不要求：

V_R = \bigsqcup_i B_i.

而採用 cover：

V_R \approx \bigcup_{i=1}^{m}B_i \cup \mathfrak F_R.

8.2 Overlap 是重要資訊

對：

B_i,B_j,

定義 overlap：

O_{ij} = \frac{ \operatorname{vol}(B_i\cap B_j) }{ \operatorname{vol}(B_i\cup B_j) }.

高 overlap 可能意味：

方法族實際上共享同一核心；
obstruction 是跨 basin 的；
basin 切分太細；
一個 bridge lemma 形成共同通道。

8.3 Cross-basin traffic

定義：

T_{ij} = \sum_{\substack{u\in B_i\\v\in B_j}} w(u,v).

形成 basin traffic matrix：

\mathbf T = [T_{ij}].

若：

T_{ij}\gg0,

表示兩個 basin 之間有實際研究通道。

若：

T_{ij}\approx0,

則需要判斷：

真正結構分離；
corpus 缺邊；
retriever 沒找到；
研究者根本沒試過。

8.4 Basin-level entropy

令近期研究在 basin 上的分布為：

p_i(N,W).

定義：

H_B(N,W) = - \sum_i p_i\log p_i.

低 entropy：

H_B\downarrow

表示研究高度集中。

但低 entropy 不一定壞。

若某 basin 正在產生高 audited yield：

\rho_k\gg0,

集中可能是合理 exploit。

只有當：

H_B\downarrow

與：

\rho_k\downarrow

長期同時成立，才更像「被困」。

9. Exploration--Exploitation 不能簡化成「多試幾條」

9.1 大搜尋空間中的經典困境

formal theorem proving 的 action space 很大。

在 proof state：

s_t,

模型可以產生大量 tactic：

a_t^{(1)},a_t^{(2)},\ldots.

若每個 tactic 再分支，搜尋樹快速膨脹。

因此所有 prover 都必須在：

\text{exploration}

與：

\text{exploitation}

間取捨。

9.2 BFS-Prover：深路徑也需要被刻意鼓勵

BFS-Prover 顯示，簡單 best-first tree search 若配合適當的 expert iteration、compiler feedback 與 length normalization，可以有效提升大型 Lean proof search。

對本文而言，重要的不是其 benchmark 排名，而是：

\boxed{ \text{search policy itself changes which region becomes reachable}. }

如果一個 policy 系統性偏好短 proof，則某些需要先繞遠的 basin 會被壓低。

因此：

\text{unvisited}

不等於：

\text{unproductive}.

9.3 FETCH：過度探索和探索不足可以同時存在

FETCH 的分析尤其重要。

它區分：

\text{over-exploration}

來自大量語義等價／重複狀態；

以及：

\text{under-exploration}

來自 verifier score 高 variance 導致軌跡頻繁切換。

這兩者可以同時發生：

系統花很多算力，但既重複走舊路，又沒有把真正的新路走深。

因此「生成量巨大」不能直接當 coverage 指標。

9.4 FormalEvolve：固定預算下，多樣性本身是可優化量

FormalEvolve 把 autoformalization 設計成：

\text{budgeted repertoire search}.

它不只追求一個可編譯候選，而是維持 diverse candidate repertoire，並測量 cross-problem coverage concentration。

這為本文提供直接啟發：

\boxed{ \text{proof-space observatory should track diversity distribution, not only success count}. }

10. 局部 premise 和全域 premise：另一種 basin 盲點

10.1 單步最相關不等於整體最必要

LeanSearch v2 提出 global premise retrieval：

一個研究級 theorem 往往需要一組分散在 library 各處、聯合起來才足夠的 lemma。

因此：

\operatorname{TopK}(s_t)

的局部 premise selection 不必等於：

P^\star(Q)

這個完整 proof 所需的 premise set。

10.2 Premise basin

如果 retriever 長期只回傳同一高相關 cluster：

P_1,

研究系統會形成：

B_{\mathrm{premise}}(P_1).

即使該 cluster 內搜尋非常深入，也可能一直缺：

p^\star \notin P_1.

這時候局部 proof search 會呈現：

高 recurrence；
高 lemma reuse；
高 internal connectivity；
長期無 closure。

但問題不一定是 proof strategy。

可能只是：

\boxed{ \text{premise basin lock-in}. }

10.3 Global retrieval 作為 basin escape

LeanSearch v2 的 sketch--retrieve--reflect 類型流程，可被重新解讀為：

B_i \rightarrow \text{global premise query} \rightarrow B_j.

這不是說 LeanSearch v2 在研究 basin theory。

而是它提供一個工程案例：

改變 retrieval level 本身可以改變可達 proof space。

11. Blueprint、DAG 與 dead-end basin

11.1 Goedel-Architect 的全局視角

Goedel-Architect 不是只逐步遞歸拆 lemma。

它先建立 definitions / lemmas 的 dependency blueprint：

\mathcal B_Q.

若某些 lemma proof 失敗，失敗會回饋到 blueprint refinement。

這件事對 proof-space dynamics 很重要。

因為：

\text{failure}

不只是葉節點錯誤。

它可以改變：

\text{global route architecture}.

11.2 Dead-end strategy

若一個 route family：

R_a

反覆產生：

O_a

而 blueprint 層知道：

R_a\rightarrow O_a

已經多次重現，系統就不必無限在低階 tactic 層重跑。

這正是：

\boxed{ \text{basin-level memory}. }

它把：

\text{this tactic failed}

提升成：

\text{this strategy family has a known recurrent obstruction under these assumptions}.

11.3 Basin memory 是避免計算浪費的必要條件

如果沒有 basin memory：

\text{failure}_1, \text{failure}_2, \ldots

只會變成大量局部 log。

如果有：

O_{\mathrm{ID}},

則可以建立：

\operatorname{Avoid}(B,O_{\mathrm{ID}},\mathcal H).

或：

\operatorname{Escape}(B,O_{\mathrm{ID}}).

這是從 theorem prover 走向 research observatory 的關鍵差異。

12. TreeThink 與「搜尋方法本身」的可交換性

12.1 不同 search algorithm 會看到不同空間切片

TreeThink 將：

BFS；
beam；
MCTS；

等 search strategy 模組化，並可搭配不同 evaluator。

這提醒我們：

\Omega^{\mathrm{obs}}_R

其實高度依賴：

R.

如果：

R_1 \neq R_2,

則：

\Omega^{\mathrm{obs}}_{R_1} \neq \Omega^{\mathrm{obs}}_{R_2}

完全合理。

12.2 因此飽和必須帶 regime index

本文拒絕寫：

\operatorname{Sat}(Q).

更合理的是：

\operatorname{Sat}(Q\mid R).

進一步：

S_K(B\mid R,N,W).

只要模型、retriever、方法族或 verifier 改變：

R\rightarrow R',

舊的 saturation label 就必須重新評估。

13. Representation basin：換句話說，有時候你不是卡在證明，而是卡在語言

13.1 同一命題的 representation 不一定等難

LSI-PSD-03 已討論：

x\sim y

在數學語義上等價，不代表：

\operatorname{Cost}_{\mathrm{search}}(x) = \operatorname{Cost}_{\mathrm{search}}(y).

因此一個 proof basin 可能其實是 representation basin。

13.2 Representation lock-in

若長程 corpus 形成固定語言：

\mathcal L_1,

retriever、prompt、lemma naming、obstruction taxonomy 都會逐漸適應：

\mathcal L_1.

這會降低換到：

\mathcal L_2

的短期效率。

於是研究系統可能錯誤得出：

$\mathcal L_2$ 沒用。

實際上只是：

\text{switching cost}>0.

13.3 Escape intervention 必須給新 representation 成熟時間

因此測：

\Gamma_{\mathrm{esc}}

時不能只看一次生成。

應設：

W_{\mathrm{adapt}}>0.

先允許：

vocabulary adaptation；
premise re-indexing；
theorem translation；
verifier bridge；
agent memory migration。

然後再比較長期 yield。

14. Method basin：同一套成功方法可以把自己變成盲點

14.1 方法族的自我強化

設：

\mathcal M_1

曾經產生大量有效結果。

系統會自然提高：

P(\mathcal M_1\mid Q,\mathcal H).

這在貝氏意義上不是不合理。

但是如果 posterior 太快坍縮：

P(\mathcal M_j)\rightarrow0 \qquad j\neq1,

則研究失去探索能力。

14.2 方法多樣性

定義近期 method-family distribution：

p_m.

方法 entropy：

H_M = - \sum_m p_m\log p_m.

若：

H_M\downarrow

且：

\rho_k\downarrow,

應啟動 method diversification。

若：

H_M\downarrow

但：

\rho_k\gg0,

則可能只是合理集中。

所以 entropy 不能獨立判讀。

14.3 Forced ablation

一個強測試是暫時禁用高中心度方法：

\mathcal M_{\max}.

比較：

\rho_k^{(-\mathcal M_{\max})}

與：

\rho_k^{(\mathrm{full})}.

如果禁用後 novelty 上升，說明原系統可能有 method lock-in。

如果禁用後全面崩潰，則高中心度方法可能真的承擔重要結構。

15. Resource basin：資源不足也會偽裝成局部飽和

15.1 固定 budget 會截斷深路徑

對一個 proof route：

r,

若所需成本：

C(r)>\mathcal B,

則在目前制度下：

r

永遠無法完整展開。

長期看起來會像：

\text{recurrent partial progress} \rightarrow \text{same obstruction}.

但真正原因可能只是：

\boxed{ \text{budget ceiling}. }

15.2 Resource escalation test

令：

\mathcal B_1<\mathcal B_2<\cdots.

測：

\rho_k(B\mid\mathcal B_j).

如果：

\rho_k

隨 budget 增加顯著恢復，則原飽和標記應被撤回或降級。

若在大幅 resource escalation 後仍沒有變化，才增加「方法／表示瓶頸」的相對可信度。

但仍不能推出原命題錯誤。

16. Evaluator basin：評分器可能把搜尋困在自己的偏好中

16.1 Proof search 不只由 generator 決定

搜尋決策通常依賴：

V(s),

或：

P(a\mid s).

若 evaluator 偏好某類短、熟悉、局部可驗證的狀態，可能壓低長期高價值 route。

16.2 Evaluator ensemble

一個實驗方法是建立：

V_1,V_2,\ldots,V_m.

比較不同 evaluator 下：

\mathcal G_R^{(i)}.

若 basin 結構對 evaluator 高度敏感：

B^{(1)} \neq B^{(2)},

則「局部飽和」很可能有 instrument dependence。

16.3 Instrument dependence 不等於沒有真結構

科學觀測本來就有儀器依賴。

重點不是要求：

\mathcal G_R

完全客觀。

而是要求：

\boxed{ \text{instrument dependence be measured and declared}. }

17. 時間、順序與研究歷史本身會塑造 basin

17.1 Path dependence

令研究歷史：

\mathcal H_N = (g_1,\ldots,g_N).

下一輪策略：

\pi_{N+1} = \Pi(Q,\mathcal H_N).

所以：

\mathcal H_N

不只是紀錄。

它是搜尋動力的一部分。

17.2 重排實驗

可對 corpus 做 random permutation：

\sigma(\mathcal H_N).

但必須注意：

真實研究不能真的把歷史重排。

Permutation test 只能回答統計問題，例如：

\text{observed novelty trend}

是否超過順序隨機化的基線。

它不能模擬「如果研究歷史真的不同，AI 會走哪裡」。

17.3 Forked-history experiment

更強的測試是：

從某 checkpoint：

H_t

建立多個 fork：

H_t^{(1)}, H_t^{(2)}, \ldots,H_t^{(m)}.

給不同方法政策。

比較：

B^{(1)}_{t+\Delta}, \ldots, B^{(m)}_{t+\Delta}.

這能直接測：

\text{basin dependence on research history}.

18. NS-203：為什麼它目前更像「局部高階採樣」而不是「全域耗盡」

18.1 Corpus accounting

NS Proof-Space Sampling Observatory v0.1 對整包遞迴掃描後得到：

1109

個 file instances，

其中：

593

個 Markdown instances，

去除 exact duplicate 後：

565

個 unique Markdown artifacts。

保守排除：

README；
CHANGELOG；
SOURCE_POLICY；
checkpoint；
roadmap；
handoff；
audit；

後，得到：

\boxed{ 203 }

份 NS paper-like artifacts。

18.2 高階採樣 tier

v0.1 的操作性 tier 分布為：

T_1=84,

T_2=107,

T_3=10,

T_X=2.

這顯示 corpus 已存在大量：

\text{route revisit}.

而少數支線進入：

\text{confluence / higher-order family analysis}.

18.3 但全域 novelty collapse 沒有被建立

累積 nearest-neighbor novelty 從早期下降到後期，看似支持飽和。

但累積比較池會隨時間變大，因此有 size bias。

固定窗口：

W=20

後，得到：

\bar\nu_{\mathrm{Q2}}=0.5425,

\bar\nu_{\mathrm{Q4}}=0.5781.

不是後期更低。

500 次 permutation baseline 得：

z\approx1.01.

因此 v0.1 沒有支持：

\boxed{ \text{whole-corpus monotone novelty collapse}. }

18.4 這反而正好支持本文的問題設定

如果 corpus 裡：

某些 X72 round 出現 obstruction confluence；
某些 DCRP 路線進入 second-order / higher-order residue；
C5-H 出現 all-order escalation；
多個 series 反覆命中 carrier-supplier、rigidity-closure、obstruction-gap-defect；

同時整體固定窗 novelty 沒崩塌，

那最自然的候選模型正是：

\boxed{ \text{localized basin saturation + globally open observed corpus}. }

18.5 不能從 NS-203 推出什麼

不能推出：

\text{Navier--Stokes is misframed}.

不能推出：

\text{Navier--Stokes is unprovable}.

不能推出：

\text{the Clay problem is badly defined}.

不能推出：

\text{AI has exhausted known mathematics}.

目前只可以說：

在這個特定 AI 長程研究 corpus 中，某些方法／概念／障礙區域顯示高 recurrence 與高階再採樣，而整個 corpus 尚未顯示穩健的全域 novelty collapse。

這是 observational claim。

19. 從 concept family 到 basin：第二版 observatory 應如何升級

19.1 v0.1 的限制

目前 concept family 如：

\text{carrier-supplier},

\text{rigidity-closure},

\text{obstruction-gap-defect}

仍然是 routing ontology。

它們不能直接當 basin。

因為同一 broad family 可能包含多個不等價的 theorem state。

19.2 Canonical obstruction ID

第二版應建立：

OBSTRUCTION_ID
ASSUMPTIONS
DOMAIN
NORMALIZED_STATEMENT
TERMINAL_STATUS
PROOF_DEPENDENCIES
COUNTEREXAMPLE_STATUS
AUDIT_LEVEL

若兩個 artifact 只有在：

\text{normalized assumptions}

與：

\text{terminal obstruction}

都被確認等價後，才允許合併。

19.3 Basin graph

建立：

G_O = (V_O,E_O),

其中：

V_O = \{\text{audited obstruction / route states}\}.

再以：

recurrence；
shared dependencies；
transfer；
confluence；

建立 basin。

這會比 title embedding 強得多。

20. 一個可重現的 Basin Detection Protocol

20.1 Step A：建立 canonical node

對每個 artifact 抽取：

x_i = ( A_i, C_i, L_i, O_i, S_i ),

其中：

$A_i$ ：assumptions；
$C_i$ ：claims；
$L_i$ ：lemma dependency；
$O_i$ ：obstruction；
$S_i$ ：status。

20.2 Step B：先 quotient，再聚類

建立：

x_i\sim x_j.

只在 audited equivalence 後合併。

避免：

\text{cluster first} \rightarrow \text{assume equivalence later}.

20.3 Step C：建立 typed graph

邊至少分：

E_{\mathrm{derive}}, E_{\mathrm{revisit}}, E_{\mathrm{depend}}, E_{\mathrm{converge}}, E_{\mathrm{escape}}.

不要把所有關係壓成單一 similarity edge。

20.4 Step D：候選 basin

使用多種 community / conductance 方法產生候選：

B_1,\ldots,B_m.

但 algorithm 只負責：

\text{candidate generation}.

最終 basin label 仍需 structural audit。

20.5 Step E：計算多階 yield

對每個 basin：

\rho_0,\rho_1,\ldots,\rho_K.

再配：

R_W,\phi,H_B,H_M.

20.6 Step F：主動 escape

如果：

S_K(B)=1,

則至少觸發數個不同類型 escape：

a_1,\ldots,a_m.

例如：

representation switch；
premise-globalization；
method ablation；
resource escalation；
model-family change。

20.7 Step G：再判定

只有當多種 escape 都沒有帶來：

\Gamma_{\mathrm{esc}}>0

時，才把 saturation confidence 上調。

仍然不能上調成：

\text{unprovability confidence}=1.

21. Saturation Confidence：把「看起來飽和」變成分級證據

21.1 分數

定義：

C_{\mathrm{sat}}(B) = f( \rho, R_W, \phi, D_{\mathrm{audit}}, E_{\mathrm{attempt}}, E_{\mathrm{escape}}, R_{\mathrm{robust}} ).

其中：

$D_{\mathrm{audit}}$ ：人工／形式稽核深度；
$E_{\mathrm{attempt}}$ ：有效嘗試量；
$E_{\mathrm{escape}}$ ：escape intervention 多樣性；
$R_{\mathrm{robust}}$ ：對模型、retriever、順序、budget 的穩健度。

21.2 建議分級

Level 0：未評估

資料不足。

Level 1：表面 recurrence

文字／概念重複增加。

Level 2：route recurrence

audited route 重訪。

Level 3：multi-order recurrence

多階 novelty yield 同時下降。

Level 4：escape-resistant local saturation

多種 escape intervention 後仍低 yield。

Level 5：regime-bounded global observational saturation

固定 $R$ 的已知 basin cover 全部高度飽和，frontier expansion 反覆失敗。

即使 Level 5，也不叫：

\text{mathematical exhaustion}.

22. 「全域開放」也不能被浪漫化

22.1 新東西很多不代表研究健康

若系統不停製造：

\text{new terms},

\text{new symbols},

\text{new reformulations},

但：

\rho_k\approx0,

則「看似開放」只是語言膨脹。

因此 global openness 需要 audited novelty。

22.2 Frontier quality

對 frontier candidate：

f

定義：

Q_F(f) = g( \text{semantic distance}, \text{formal validity}, \text{dependency novelty}, \text{obstruction novelty}, \text{transfer potential} ).

只有：

Q_F(f)>\tau_F

才進入高優先級 frontier。

22.3 Open-ended 不是無限輸出

本文不把：

\text{open}

等同：

\text{unbounded text generation}.

更合理的是：

\boxed{ \text{open} = \text{the system can still produce audited structural renewal under intervention}. }

23. 局部飽和與「越是真理越可能像廢話」的關係

23.1 不在本文提前證明後續命題

後續 LSI-PSD-07 將處理：

\text{truth--generativity inversion}.

本文只指出一個接口。

如果 basin 在不斷加入約束後：

B_0\supset B_1\supset\cdots,

可能出現：

H(B_t)\downarrow.

極端時：

|B_t|\rightarrow1.

那麼最後留下的核心命題可能表面非常簡單。

23.2 但局部簡化不等於全域真理

若某 basin 壓縮成：

x^\star,

只能說：

\text{within this basin and regime, the survivor structure is simple}.

不能推出：

x^\star = \text{ultimate mathematical truth}.

這個區分會在後續「真理—生成性反轉」與「生產性錯置」兩篇變得非常重要。

24. 局部飽和與問題範疇錯置的關係

24.1 Saturation 可以觸發 framing audit

如果：

S_K(B)=1

且多種 escape：

a_1,\ldots,a_m

都失敗，

系統可以提高：

\operatorname{Priority}(\text{framing audit}).

24.2 但不能直接診斷 framing error

必須保持：

\boxed{ S_K(B) \not\Rightarrow \operatorname{Misframed}(Q). }

因為同樣現象也可能來自：

問題真的極難；
所需新理論尚未出現；
proof 太長；
resource 不夠；
verifier 不夠表達；
intelligence 不夠；
independence；
命題為假但反例未找到。

24.3 Framing audit 是下一步，不是結論

因此流程應是：

\text{local saturation} \rightarrow \text{audit trigger} \rightarrow \text{alternative hypotheses},

而不是：

\text{local saturation} \rightarrow \text{question is wrong}.

25. 多模型、多方法與獨立研究線的真正作用

25.1 多 AI 不只是多投票

若所有 agent 使用：

\text{same prompt},

\text{same retrieval},

\text{same model family},

\text{same proof memory},

那：

n\text{ agents}

可能只是在同一 basin 裡並行採樣。

25.2 Independent basin probes

更好的設計是：

R_1,\ldots,R_m

有意做差異：

model family；
method family；
representation；
premise retriever；
proof language；
allowed tools；
memory subset。

比較：

\mathcal G_{R_1}, \ldots, \mathcal G_{R_m}.

25.3 交集和差集都重要

若多個 regime 都命中：

O^\star,

則：

O^\star

的 obstruction robustness 上升。

若：

B^{(1)}

只在某個 regime 出現，則可能是：

新發現；
representation artifact；
instrument artifact。

都值得研究。

26. 一個最小 Proof-Basin Observatory Schema

problem:
  id: Q
  statement: ...
  formalization: ...
  domain: ...

regime:
  axioms: ...
  language: ...
  methods: ...
  verifier: ...
  model: ...
  retriever: ...
  budget: ...
  memory_version: ...

node:
  id: ...
  order: 0
  assumptions: ...
  claims: ...
  dependencies: ...
  obstruction_id: ...
  audit_status: ...
  equivalence_class: ...

edge:
  source: ...
  target: ...
  type: revisit
  audit_level: ...
  weight: ...

basin:
  id: ...
  members: ...
  conductance: ...
  recurrence_density: ...
  method_entropy: ...
  order_yield: ...
  saturation_level: ...

escape:
  id: ...
  source_basin: ...
  action_type: representation_switch
  destination: ...
  audited_gain: ...
  status: ...

這樣才可能讓：

\text{basin}

成為可重跑資料，而不是聊天中的比喻。

27. 對未來 AI 自主數學研究的架構含義

27.1 Agent 應該知道自己在哪個 basin

下一代數學 agent 不只需要：

下一步做什麼？

還要知道：

我現在是不是又回到過去研究過的 basin？

因此狀態應包含：

b_t = \operatorname{BasinID}(s_t).

27.2 Agent 應知道 basin 的歷史

例如：

Basin B-17
attempts: 492
audited novel classes: 8
last 100 yield: 0.01
known obstructions: O-31, O-44
escape attempts:
  - representation switch: failed
  - premise globalization: positive
  - budget x4: neutral

這種記憶比單純：

以前試過。

強得多。

27.3 Meta-controller

可以建立：

\Pi_{\mathrm{meta}}

決定：

\text{exploit}, \text{explore}, \text{escape}, \text{audit}, \text{stop}.

輸入：

( C_{\mathrm{sat}}, \Gamma_{\mathrm{esc}}, H_B, H_M, \rho_k, \mathfrak F_R ).

27.4 Stop 也應該分層

不是只有：

\text{proof found}

或：

\text{give up}.

而是：

stop this tactic；
stop this route；
stop this basin；
stop this regime；
pause this problem；
request new definition；
request stronger intelligence／resource；
transfer descendants elsewhere。

這會大幅改善長程研究的計算效率。

28. 實驗一：Basin Escape Benchmark

28.1 目的

測試：

當局部 audited yield 下降時，主動換 basin 是否比繼續加算力更有效？

28.2 設計

選擇已知可解但證明路徑多樣的 theorem set。

對每題建立兩組：

Control

\text{continue same regime}.

Escape

當：

C_{\mathrm{sat}}>\tau

時，強制：

representation switch；
method switch；
global premise retrieval；
random restart。

28.3 指標

比較：

P_{\mathrm{solve}},

\text{audited novel classes},

\text{tokens},

\text{verifier calls},

\text{time-to-new-basin}.

28.4 可證偽性

如果 escape 組在多個資料集上：

\Gamma_{\mathrm{esc}}\le0

且成功率沒有改善，

則本文的 basin-control 工程價值會被削弱。

29. 實驗二：局部飽和假陽性測試

29.1 人工製造 retrieval lock

刻意限制 retriever：

P_{\mathrm{retrieval}}

只在一個子庫。

觀察是否產生：

R_W\uparrow, \quad \rho\downarrow, \quad \phi\downarrow.

29.2 解鎖

再恢復 global premise retrieval。

若 novelty 迅速恢復：

\Gamma_{\mathrm{esc}}\gg0,

則證明：

相同的飽和表面現象可以純粹由搜尋制度製造。

這是本文非常重要的 calibration experiment。

30. 實驗三：多模型 Basin Agreement

30.1 問題

不同模型是否會形成相同 basin？

30.2 定義

對 model $m$ ：

\mathcal B^{(m)} = \{B_1^{(m)},\ldots\}.

定義 basin alignment：

A_{mn} = \operatorname{Match}( \mathcal B^{(m)}, \mathcal B^{(n)} ).

30.3 解讀

若：

A_{mn}\approx1

對不同架構模型都成立，

則 basin 更可能反映問題結構。

若：

A_{mn}\approx0,

則 basin 可能高度 model-specific。

兩種結果都重要。

31. 實驗四：NS-203 的第二輪 theorem-level basin audit

31.1 目標

把 v0.1：

\text{title / concept family graph}

提升成：

\text{claim--lemma--obstruction graph}.

31.2 抽樣

優先處理：

NS-DCRP；
NS-X72；
NS-MORP；
NS-FCBP；
NS-C5；
Proof Asset Map。

因為這些支線已有較高 recurrence 或 cross-series traffic。

31.3 手工 gold set

每條 route 至少抽取：

50

個 artifact pair。

雙重標註：

\text{same basin?}

\text{same obstruction?}

\text{same proof skeleton?}

\text{mere lexical similarity?}

31.4 成功條件

若自動 basin detector 對 gold set：

F1>0.8

並且 escape intervention 能穩定找出新 audited classes，

則可以開始談更強的 empirical proof-space dynamics。

32. Basin 與 SDPE：空間域證明包圍的局部版本

32.1 原始 filtration

SDPE 型思路可寫成：

\Omega_{t+1} = \Omega_t\cap H_t.

每個 audited no-go：

H_t

切除不可能區域。

32.2 多 basin filtration

本文改成：

B_i^{(t+1)} = B_i^{(t)} \cap H_t.

不同 theorem cut 只影響部分 basin。

甚至可能：

H_t

同時：

壓縮 $B_1$ ；
不影響 $B_2$ ；
打開 $B_3$ 的新 bridge。

因此 proof enclosure 不是單調「整塊空間縮小」的唯一圖像。

更一般的是：

\boxed{ \text{local contraction + basin splitting + bridge creation + frontier renewal}. }

32.3 研究過程可以改變空間的有效座標

如果新 theorem 建立：

B_1\sim B_2,

兩 basin 可以 merge。

如果反例顯示原先同一 family 其實分成：

B_{1a},B_{1b},

則 basin split。

因此 observatory 本身需要版本化：

\mathcal G_R^{(0)} \rightarrow \mathcal G_R^{(1)} \rightarrow \cdots.

33. 失敗不是垃圾：Escape Failure Atlas

33.1 為什麼要保存失敗 escape

如果研究者只保留：

\text{successful escape},

未來系統可能反覆嘗試同一失敗跨越。

因此要建立：

\mathcal E_{\mathrm{fail}}.

33.2 Failure type

建議分類：

translation failure；
semantic mismatch；
verifier incompatibility；
no new premise；
same obstruction recurrence；
new obstruction；
budget failure；
evaluator failure；
representation degeneration；
proof-state explosion。

33.3 高階價值

若多個 basin 的 escape 都反覆落在：

O^\star,

則：

O^\star

本身可能成為高階 confluence obstruction。

也就是：

\text{escape failure} \rightarrow \text{new proof-space relation}.

34. 從「局部盆地」到「研究地圖」

34.1 最終 observatory 應該顯示什麼

不是一張漂亮的 force-directed graph。

而至少應同時顯示：

basin；
basin saturation level；
frontier；
known obstructions；
escape attempts；
cross-basin traffic；
method／representation distribution；
confidence；
unresolved ambiguity。

34.2 地圖上的顏色不能冒充真值

視覺上：

紅色 = 飽和

只應表示：

C_{\mathrm{sat}}>\tau.

不能表示：

此路徑數學上已證明不可能。

因此 UI 必須直接顯示：

SATURATION TYPE:
observational / local / regime-bounded

NOT A CLAIM OF:
falsehood / unprovability / independence

35. 形式命題總表

命題 1：局部飽和非傳播

\boxed{ S_K(B) \not\Rightarrow S_K(V_R). }

命題 2：觀測全域飽和非數學全域耗盡

\boxed{ \operatorname{Sat}^{R,K}_{\mathrm{global,obs}} \not\Rightarrow \Omega^{\mathrm{math}}\text{ exhausted}. }

命題 3：低 novelty 非充分條件

\boxed{ \nu\downarrow \not\Rightarrow S_K(B)=1. }

命題 4：低採樣不能叫飽和

\boxed{ A_k\approx0 \not\Rightarrow \rho_k\approx0\text{ means saturation}. }

命題 5：成功 basin 不等於完整空間

\boxed{ \operatorname{Success}(B)\uparrow \not\Rightarrow V_R=B. }

命題 6：搜尋制度改變可達空間

\boxed{ R_1\neq R_2 \Rightarrow \Omega^{\mathrm{obs}}_{R_1} \text{ may differ from } \Omega^{\mathrm{obs}}_{R_2}. }

命題 7：Escape gain 是局部研究續行決策的證據

\boxed{ \Gamma_{\mathrm{esc}}>0 }

支持從原 basin 轉向新區域，但不保證新區域最終可閉合目標 theorem。

命題 8：多 basin recurrence 比單一文本重複更有診斷價值

若獨立方法／表示：

B_i

反覆匯流至同一 audited obstruction：

O^\star,

則：

\operatorname{Robustness}(O^\star)\uparrow.

但仍：

O^\star \not\Rightarrow \text{unprovability}.

36. 非主張總表

本文不主張：

proof space 在數學本體上天然具有唯一 basin decomposition；
graph conductance 是證明空間的唯一正確幾何；
embedding community 等於數學等價類；
局部 novelty 下降就是 saturation；
多階 recurrence 就代表接近真理；
basin escape 一定比加算力有效；
多模型共識等於數學真理；
NS-203 已耗盡 Navier--Stokes 研究空間；
NS-203 證明 Clay 問題 framing 有錯；
P/NP 或 NS 必然不可判定；
regime-bounded saturation 可推出 Gödel 式獨立性；
目前 AI 智能足以列舉所有重要表示；
frontier 為空表示沒有未知區域；
新 representation 一定更好；
研究地圖可以取代 theorem-level verification。

37. 與前四篇的整合

LSI-PSD-01 建立：

\text{search regime} \neq \text{mathematical reality}.

LSI-PSD-02 建立：

I_N = \text{proof-space coverage functional}.

LSI-PSD-03 要求先在：

\Omega/\sim

上去除表面重複。

LSI-PSD-04 再把採樣分成：

\Omega^{(0)}, \Omega^{(1)}, \Omega^{(2)}, \ldots.

本文進一步指出：

即使每個階都能計量，也不能假設整個空間均勻被採樣。

因此：

I_k

必須分解成 basin-conditioned quantities：

I_k = \sum_i I_{k,i} + I_{k,\mathfrak F}.

更一般地，若 basin overlap：

I_k

需要 inclusion--exclusion 或 probabilistic cover correction。

所以真正成熟的 proof-space integration 不只是：

\Delta I_k(N).

而是：

\boxed{ \Delta I_k(B_i,N) }

與：

\boxed{ \Delta I_k(\mathfrak F,N). }

38. 一個更完整的動力圖像

研究開始時：

\mathfrak F \gg B_i.

大量區域尚未展開。

中期：

B_1,B_2,\ldots

逐漸形成。

某些 basin：

\rho_k>0

仍有高產量。

後期局部：

\rho_k(B_1)\rightarrow0.

若系統沒有 meta-control，就會：

B_1\rightarrow B_1\rightarrow B_1.

如果有：

\Pi_{\mathrm{meta}},

則：

B_1 \xrightarrow{\mathrm{escape}} B_j

或：

B_1 \rightarrow \mathfrak F.

於是長程研究不再是一條：

\text{linear paper sequence},

而是一個：

\boxed{ \text{basin formation--saturation--escape--renewal process}. }

39. 對 AI 海戰術的修正

39.1 單純增加 agent 數量會遇到 basin crowding

若：

n\rightarrow10^4

但所有 agent 都在：

B_1,

那麼新增算力可能主要提高：

\text{sampling density},

不是：

\text{coverage breadth}.

39.2 真正需要的是 basin allocation

設：

n_i

為分配到 basin $B_i$ 的 agent 數。

應解：

\max_{\{n_i\}} \sum_i \mathbb E[ U_i(n_i) ]

subject to：

\sum_i n_i=N.

其中：

U_i

不是 paper count，而是 audited novelty utility。

39.3 自適應 allocation

若：

\rho(B_i)\downarrow,

則：

n_i\downarrow.

若：

\Gamma_{\mathrm{esc}}(B_i,a)>0,

則增加對新 basin 的 allocation。

這才是真正的：

\boxed{ \text{proof-space resource scheduling}. }

40. 與未來第 6 篇的接口：障礙匯流

本文主要回答：

哪裡在局部飽和？

下一篇將集中問：

為什麼不同 basin／route 最後會撞上同一 obstruction？

如果：

B_1\rightarrow O,

B_2\rightarrow O,

B_3\rightarrow O,

則：

O

不再只是某條 proof 的局部失敗。

它可能是：

\boxed{ \text{cross-basin confluence hub}. }

因此 LSI-PSD-06 將建立：

obstruction canonicalization；
weighted confluence；
route-family convergence；
obstruction inheritance；
no-go region；
escape obstruction；
confluence graph。

這會把本文的 basin map 進一步變成 obstruction map。

41. 結論

長程 AI 數學研究最容易產生的一個錯覺是：

我已經研究這個問題非常久，所以我大概已經看完這個問題。

本文的核心工作就是拆掉這個推論。

在一個巨大的 proof space 中，研究可以非常深入地探索某個局部區域：

B.

系統可以在其中生成上百篇論文、數千個 lemma、反覆形成二階、三階與更高階 relation，甚至建立 all-order no-go family。

這只足以支持：

\boxed{ \text{this basin is highly explored}. }

若 audited yield 同時長期下降，可以進一步支持：

\boxed{ \text{this basin is operationally locally saturated}. }

但仍不能推出：

\boxed{ \text{the proof space is globally exhausted}. }

更不能推出：

\boxed{ \text{the mathematical problem is wrong}. }

因此成熟的 AI 研究系統不應只追求：

\text{more generations}.

也不應只追求：

\text{more compute}.

它必須知道：

\boxed{ \text{where it has been, where it keeps returning, where novelty is dying, and what has never been seriously tried}. }

真正的長程研究控制迴路應是：

\boxed{ \text{sample} \rightarrow \text{quotient} \rightarrow \text{map} \rightarrow \text{detect basin} \rightarrow \text{measure local yield} \rightarrow \text{escape} \rightarrow \text{audit renewal}. }

從這個角度看，proof-space saturation 不是一個「最後宣布失敗」的詞。

它是一個路由訊號。

它告訴研究系統：

這裡可能已經看得夠深了；下一個問題不是再多走一百次，而是確認世界是否還有別的入口。

這也構成本文最終命題：

\boxed{ \textbf{A mature proof-search system must distinguish depth within a basin from breadth across proof space.} }

以及其認識論底線：

\boxed{ \textbf{Local saturation is a property of an observed research region, not a verdict on mathematical reality.} }

參考文獻

Yin, D., & Gao, J. (2025). Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs. arXiv:2503.04772. https://arxiv.org/abs/2503.04772
George, R. J., Huang, S., Song, P., & Anandkumar, A. (2025; revised 2026). LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction. arXiv:2502.17925. https://arxiv.org/abs/2502.17925
Xin, R. et al. (2025). BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving. arXiv:2502.03438. https://arxiv.org/abs/2502.03438
Wang, A. et al. (2025). Don't Get Lost in the Trees: Streamlining LLM Reasoning by Overcoming Tree Search Exploration Pitfalls. arXiv:2502.11183. https://arxiv.org/abs/2502.11183
Lu, H., Wang, W., & Liu, J. (2026). FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse and Prover-Effective Autoformalization. arXiv:2603.19828. https://arxiv.org/abs/2603.19828
Gao, G. et al. (2026). LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving. arXiv:2605.13137. https://arxiv.org/abs/2605.13137
Chung, J.-H. et al. (2026). Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement. arXiv:2606.06468. https://arxiv.org/abs/2606.06468
Akbudak, B. S., Ulusan, Z. A., Erer, C. S., & Şahin, G. G. (2026). TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs. arXiv:2607.11258. https://arxiv.org/abs/2607.11258
Kung, P. N. et al. (2026). LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks. arXiv:2606.03303. https://arxiv.org/abs/2606.03303
Zhang, Y. et al. (2026). LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization. arXiv:2606.05400. https://arxiv.org/abs/2606.05400
Kurgan, S. et al. (2026). TheoremGraph: Bridging Formal and Informal Mathematics. arXiv:2606.25363. https://arxiv.org/abs/2606.25363
EveMissLab / Neo.K × AI collaborative analysis (2026). NS Proof-Space Sampling Observatory v0.1. Internal reproducible corpus analysis, 2026-08-17.

附錄 A：符號表

符號	意義
$Q$	研究問題
$R$	搜尋制度 / research regime
$\Omega_R^{\mathrm{obs}}(Q)$	在 $R$ 下實際可觀測研究空間
$\Omega^{\mathrm{math}}(Q)$	理想化的底層數學證明空間；本文不假定可直接觀測
$\mathcal G_R(Q)$	quotient 後的加權 typed research graph
$B$	操作性 proof basin
$\phi(B)$	basin conductance
$R_W(B)$	固定窗口 recurrence density
$A_k(B;N,W)$	第 $k$ 階嘗試數
$U_k(B;N,W)$	第 $k$ 階新 audited equivalence classes
$\rho_k(B;N,W)$	第 $k$ 階 audited yield
$S_K(B)$	$K$ 階局部飽和標記
$\mathfrak F_R(N)$	觀測 frontier
$\Gamma_{\mathrm{esc},k}$	第 $k$ 階 basin escape gain
$H_B$	basin allocation entropy
$H_M$	method-family entropy
$C_{\mathrm{sat}}$	saturation confidence
$\mathbf T$	cross-basin traffic matrix
$O_{ij}$	basin overlap
$\Pi_{\mathrm{meta}}$	meta-level research routing controller

附錄 B：最小實驗矩陣

實驗	控制變數	Intervention	主要指標
Basin Escape	model / theorem set	representation / method switch	$\Gamma_{\mathrm{esc}}$
Retrieval Lock	prover / budget	local vs global premise	$\rho_k$ , success
Resource Escalation	method / representation	budget multipliers	$\rho_k(\mathcal B)$
Model Agreement	theorem set / tools	model family	basin alignment
Evaluator Sensitivity	generator / corpus	evaluator	basin robustness
History Fork	checkpoint	different route policy	basin divergence
NS-203 Audit	corpus	theorem-level canonicalization	precision / recall / F1

附錄 C：Observatory 判定流程

INPUT:
  problem Q
  regime R
  research history H

1. Normalize artifacts
2. Build semantic quotient
3. Extract typed route graph
4. Generate candidate basins
5. Audit basin membership
6. Measure:
   - recurrence
   - conductance
   - order-conditioned novelty
   - audited yield
7. If local saturation candidate:
   trigger escape interventions
8. Recompute yield
9. Store success/failure trace
10. Update basin map
11. Never convert observational saturation
    into a theorem about mathematical reality

附錄 D：一句話版本

\boxed{ \text{在一口井裡挖到一萬公尺深，不代表你已經走遍整個地表。} }

對長程 AI 數學研究而言：

\boxed{ \text{depth within a proof basin} \neq \text{breadth across proof space}. }

LSI-PSD-05 — 局部飽和與全域開放：證明空間的多盆地結構

LSI-PSD-05 — 局部飽和與全域開放：證明空間的多盆地結構

Local Saturation and Global Openness: A Multi-Basin Structure of Proof Space

摘要

1. 問題的提出：為什麼「整體新奇度」是一個危險的單一指標

1.1 長程研究不會均勻覆蓋證明空間

1.2 同一個區域可以很深，但旁邊仍然很空

1.3 研究越成功，越容易被自己的成功困住

2. 從單一空間改成加權研究圖

2.1 可觀測證明空間

2.2 語義 quotient 後的節點

2.3 邊的型別

2.4 不把圖本身當作本體

3. 操作性 basin：什麼叫「研究被困在一個局部區域」

3.1 Basin 不應只靠 embedding cluster 定義

3.2 操作性 basin 定義

3.3 Conductance

3.4 Recurrence density

4. 局部飽和必須是多條件，而不是「最近看起來都一樣」

4.1 單一 novelty 不足

4.2 第 kkk 階 audited yield

4.3 多階局部飽和

4.4 低產量和飽和是不同的

5. 局部飽和非傳播原則

5.1 核心命題

5.2 更強的防誤推論形式

5.3 Regime-bounded global saturation

6. 全域開放：什麼情況下可以說「還有地方沒走」

6.1 Frontier

6.2 Frontier 不是「未知的全部」

6.3 觀測性開放證書

7. Basin escape：研究不只是繼續走，也要知道何時換區域

7.1 Escape action

7.2 Escape gain

7.3 Escape 可以失敗，而且失敗也有資訊

8. 多盆地結構：證明空間更像 cover，而不是單一區塊

8.1 不要求 basin 互斥

8.2 Overlap 是重要資訊

8.3 Cross-basin traffic

8.4 Basin-level entropy

9. Exploration--Exploitation 不能簡化成「多試幾條」

9.1 大搜尋空間中的經典困境

9.2 BFS-Prover：深路徑也需要被刻意鼓勵

9.3 FETCH：過度探索和探索不足可以同時存在

9.4 FormalEvolve：固定預算下，多樣性本身是可優化量

10. 局部 premise 和全域 premise：另一種 basin 盲點

10.1 單步最相關不等於整體最必要

10.2 Premise basin

10.3 Global retrieval 作為 basin escape

11. Blueprint、DAG 與 dead-end basin

11.1 Goedel-Architect 的全局視角

11.2 Dead-end strategy

11.3 Basin memory 是避免計算浪費的必要條件

12. TreeThink 與「搜尋方法本身」的可交換性

12.1 不同 search algorithm 會看到不同空間切片

12.2 因此飽和必須帶 regime index

13. Representation basin：換句話說，有時候你不是卡在證明，而是卡在語言

13.1 同一命題的 representation 不一定等難

13.2 Representation lock-in

13.3 Escape intervention 必須給新 representation 成熟時間

14. Method basin：同一套成功方法可以把自己變成盲點

14.1 方法族的自我強化

14.2 方法多樣性

14.3 Forced ablation

15. Resource basin：資源不足也會偽裝成局部飽和

15.1 固定 budget 會截斷深路徑

15.2 Resource escalation test

16. Evaluator basin：評分器可能把搜尋困在自己的偏好中

16.1 Proof search 不只由 generator 決定

16.2 Evaluator ensemble

16.3 Instrument dependence 不等於沒有真結構

17. 時間、順序與研究歷史本身會塑造 basin

17.1 Path dependence

17.2 重排實驗

17.3 Forked-history experiment

18. NS-203：為什麼它目前更像「局部高階採樣」而不是「全域耗盡」

18.1 Corpus accounting

18.2 高階採樣 tier

18.3 但全域 novelty collapse 沒有被建立

18.4 這反而正好支持本文的問題設定

4.2 第 $k$ 階 audited yield