# 自主數學研究代理循環

## ——結果誘導中介定理生成、逆向公理回填與知識條件化類窮舉的初步架構

**作者：Neo.K（理論構想）／Aletheia（協作整理與形式化）**  
**版本：v0.1 初版草稿**  
**日期：2026-07-09**

---

## 重要聲明

本文提出的是一套**尚未完成一般性證明、尚未完成大規模實證、尚未證明具有穩定研究增益**的自主數學研究 Agent 架構。

本文目前不主張：

$$
\mathrm{RIITG}+\mathrm{RAB}
$$

已被證明優於傳統數學研究流程、普通 backward chaining、自動定理證明器、形式證明系統、搜索型 Agent 或現有大型語言模型推理方法。

本文也不主張：

$$
\exists
\text{一般性自主數學 Agent}
$$

已經依本文架構被成功完整實現。

本文真正提出的是：

1. 一個可供未來 Agent 反覆執行的數學研究循環；
2. 一組將「生成、搜索、計算、驗證、反證、回填、重構」整合到同一動態系統中的方法論；
3. 一個以可審計、可失敗、可剪枝、可擴張知識底空間為核心的研究架構；
4. 一組可由未來實驗驗證或否證的理論命題。

因此，本文應被視為：

> **自主數學研究方法論與 Agent 架構的初版草稿。**

其價值目前主要是：

$$
\text{提出可實作結構}
+
\text{提出可測試命題}
+
\text{提出研究循環}
$$

而不是宣稱：

$$
\text{一般有效性已證明}.
$$

---

## 摘要

本文提出一套面向未來自主數學研究 Agent 的一般架構，暫稱為**自主數學研究代理循環**（Autonomous Mathematical Research Agent Loop, AMRAL）。其核心目標不是讓 Agent 對單一命題執行一次性證明，而是讓 Agent 能夠在長期迭代中反覆進行：

$$
\text{目標分析}
\rightarrow
\text{中介命題生成}
\rightarrow
\text{知識條件化類窮舉}
\rightarrow
\text{回填}
\rightarrow
\text{計算}
\rightarrow
\text{驗證}
\rightarrow
\text{反例搜索}
\rightarrow
\text{失敗分類}
\rightarrow
\text{狀態更新}
\rightarrow
\text{再次研究}.
$$

本文架構建立於前述兩個方法之上：**結果誘導的中介定理生成法**（Result-Induced Intermediate Theorem Generation, RIITG）與**逆向公理回填法**（Reverse Axiom Backfilling, RAB）。RIITG 由目標命題 $P$ 反向生成一組候選中介命題：

$$
P
\rightsquigarrow
\mathcal M,
$$

RAB 則將這些暫態橋樑命題降格為證明義務，並從既有知識、外部文獻、形式定理庫、計算結果與新引理中尋找支撐：

$$
\mathcal T
\Rightarrow
\mathcal M
\Rightarrow
P.
$$

本文進一步提出第三個核心組件：**知識條件化的證明空間類窮舉**（Knowledge-Conditioned Proof-Space Quasi-Enumeration, KCPE）。KCPE 並非暴力枚舉全部可能證明，而是在當前知識集、網路資料、已知定理、反例、計算結果、語義窗口與失敗歷史的共同約束下，動態構造有限或局部可控的候補空間：

$$
\Omega_t
=
\Omega(
P,
\mathcal K_t,
\mathcal F_{<t},
W_{\mathrm{sem}},
B_t
).
$$

其中：

- $\mathcal K_t$ ：第 $t$ 輪知識狀態；
- $\mathcal F_{<t}$ ：此前失敗記錄；
- $W_{\mathrm{sem}}$ ：語義寬度；
- $B_t$ ：計算預算；
- $\Omega_t$ ：當輪候補空間。

本文主張，真正可行的自主數學 Agent 不應只在固定知識庫內搜索，而應能在遇到缺口時主動生成：

$$
G_t
=
\operatorname{Gap}(
M_i,
T_j
),
$$

再利用網路、論文庫、形式定理庫與計算工具擴張：

$$
\mathcal K_t
\rightarrow
\mathcal K_{t+1}.
$$

因此，外部資料檢索在本文中不是「找答案」，而是**動態知識底空間擴張算子**。

本文特別強調，目前上述效益尚未被一般性證明。理論上可能的效益包括：降低無界搜索、將證明困難重新定位為少數局部節點、保留錯誤生成中的結構價值、提高失敗可觀測性、允許多 Agent 並行回填、利用計算與反例快速剪枝，以及形成可長期積累的研究狀態。本文提出多項待驗證命題，並設計可證偽條件。若未來實驗顯示該架構在多類問題上不優於基線方法，或其候補爆炸、循環、污染與回填成本無法控制，則本文方法論應被視為受限甚至失敗。

本文的核心立場是：

$$
\boxed{
\text{數學研究不必被建模為一次性證明輸出；
它可以被建模為可持續更新的計算動力系統。}
}
$$

**關鍵詞：** 自主數學 Agent、結果誘導、中介定理、逆向公理回填、知識條件化類窮舉、證明空間、動態知識底空間、AI 數學研究、計算即逼近、研究動力系統

---

# 1. 導論

## 1.1 從「證明一個命題」到「持續研究一個問題」

傳統自動定理證明問題常被簡化為：

$$
P
\rightarrow
\operatorname{Proof}(P).
$$

即：

> 給定命題 $P$ ，尋找一條合法證明。

這個模型非常重要，但它主要描述的是：

$$
\text{證明搜索}.
$$

真正的人類數學研究往往更複雜。

研究者可能會：

- 改寫問題；
- 改變表示；
- 提出中介猜想；
- 尋找反例；
- 暫時接受某個假設；
- 改證等價命題；
- 將問題縮小到特殊情況；
- 擴張使用的數學領域；
- 查找新文獻；
- 執行計算實驗；
- 發現原本問題描述錯誤；
- 拆分命題；
- 放棄某條路；
- 保留一個失敗引理；
- 多年後重新使用。

因此，數學研究更接近：

$$
\mathcal S_0
\rightarrow
\mathcal S_1
\rightarrow
\mathcal S_2
\rightarrow
\cdots
$$

其中：

$$
\mathcal S_t
$$

不是單一命題，而是整個研究狀態。

---

## 1.2 本文真正的研究對象

本文不研究：

> 某個 AI 是否能回答某道數學題。

本文研究：

> 是否能設計一套可被 Agent 長期反覆執行的數學研究循環，使其能主動生成中介命題、搜索回填、調用計算、擴張知識、尋找反例、記錄失敗並動態重構證明空間？

這個問題可以寫成：

$$
\mathcal A:
\mathcal S_t
\mapsto
\mathcal S_{t+1},
$$

其中 $\mathcal A$ 是自主研究 Agent 的狀態更新機制。

---

# 2. 前置方法

## 2.1 結果誘導的中介定理生成法

令：

$$
P
$$

為目標命題。

RIITG 不直接要求：

$$
\operatorname{Proof}(P).
$$

而先問：

> 哪些中介命題若成立，會使 $P$ 成立、近乎成立、降低難度，或產生可觀測反例？

因此：

$$
P
\overset{\mathrm{RIITG}}{\rightsquigarrow}
\mathcal M,
$$

其中：

$$
\mathcal M
=
\{M_1,\dots,M_n\}.
$$

---

## 2.2 逆向公理回填法

候選 $M_i$ 初期可以被暫時視為：

$$
A_i^\ast.
$$

但：

$$
A_i^\ast
$$

不是永久公理。

其後必須降格：

$$
A_i^\ast
\rightarrow
M_i\in\mathcal O_{\mathrm{proof}},
$$

其中：

$$
\mathcal O_{\mathrm{proof}}
$$

是證明義務集合。

再尋找：

$$
\mathcal T_i
\Rightarrow
M_i.
$$

---

## 2.3 完整方向

生成方向：

$$
P
\rightsquigarrow
M
\rightsquigarrow
T.
$$

證明方向：

$$
T
\rightarrow
M
\rightarrow
P.
$$

本文稱：

$$
\boxed{
\text{生成因果與證明因果的反向耦合}
}
$$

---

# 3. 從方法到 Agent

## 3.1 單次方法不足

若 RIITG 與 RAB 只被執行一次：

$$
P
\rightsquigarrow
\mathcal M
\leftarrow
\mathcal T,
$$

那麼它仍只是：

$$
\text{一次證明策略}.
$$

本文真正提出的是：

$$
\text{反覆執行}.
$$

即：

$$
\mathcal S_t
\rightarrow
\mathcal S_{t+1}.
$$

---

## 3.2 研究狀態

定義：

$$
\mathcal S_t
=
(
P_t,
\mathcal K_t,
\mathcal M_t,
\mathcal T_t,
\Omega_t,
\mathcal F_t,
\mathcal C_t,
\mathcal D_t
).
$$

其中：

- $P_t$ ：當前目標集；
- $\mathcal K_t$ ：知識集；
- $\mathcal M_t$ ：中介命題集；
- $\mathcal T_t$ ：候選回填支撐；
- $\Omega_t$ ：候補空間；
- $\mathcal F_t$ ：失敗記錄；
- $\mathcal C_t$ ：計算結果；
- $\mathcal D_t$ ：依賴圖或證明超圖。

---

# 4. 自主數學研究代理循環

本文提出：

> **Autonomous Mathematical Research Agent Loop**

縮寫：

$$
\mathrm{AMRAL}.
$$

基本循環為：

$$
\boxed{
\text{Analyze}
\rightarrow
\text{Generate}
\rightarrow
\text{Enumerate}
\rightarrow
\text{Retrieve}
\rightarrow
\text{Backfill}
\rightarrow
\text{Compute}
\rightarrow
\text{Verify}
\rightarrow
\text{Falsify}
\rightarrow
\text{Update}
}
$$

---

# 5. Phase A：目標分析

## 5.1 正規化

將自然語言命題轉為：

$$
P
=
Q_1x_1
\cdots
Q_nx_n
:
\Phi(x_1,\dots,x_n).
$$

---

## 5.2 生成否定

若：

$$
P
=
\forall x\in X,\ \Phi(x),
$$

則：

$$
\neg P
=
\exists x\in X,\ \neg\Phi(x).
$$

---

## 5.3 生成反例形狀

定義：

$$
W_P
=
\operatorname{Witness}(\neg P).
$$

Agent 應問：

> 若目標為假，最小可觀測證人是什麼？

---

# 6. Phase B：中介命題生成

由：

$$
P
$$

生成：

$$
\mathcal M_t.
$$

候選角色至少包括：

1. 表示橋樑；
2. 排他橋樑；
3. 不變量橋樑；
4. 正性橋樑；
5. 壓縮橋樑；
6. 局部—全域橋樑；
7. 閉包橋樑；
8. 反例證人橋樑；
9. 計算可判定橋樑；
10. 跨域映射橋樑。

---

# 7. Phase C：知識條件化類窮舉

## 7.1 為何不是暴力窮舉

完整證明空間通常極大。

若所有可寫命題集合為：

$$
\mathfrak P,
$$

則：

$$
2^{|\mathfrak P|}
$$

不可直接遍歷。

因此本文不提出：

$$
\text{full enumeration}.
$$

而提出：

> **Knowledge-Conditioned Proof-Space Quasi-Enumeration**

縮寫：

$$
\mathrm{KCPE}.
$$

---

## 7.2 候補空間

定義：

$$
\Omega_t
=
\Omega(
P_t,
\mathcal K_t,
\mathcal F_{<t},
W_{\mathrm{sem}},
B_t
).
$$

其中：

- $P_t$ ：目標；
- $\mathcal K_t$ ：知識；
- $\mathcal F_{<t}$ ：歷史失敗；
- $W_{\mathrm{sem}}$ ：語義窗口；
- $B_t$ ：預算。

---

## 7.3 類窮舉的真正含義

本文所說的「類窮舉」是：

$$
\boxed{
\text{在可控局部候補域中盡可能系統性搜索}
}
$$

而不是：

$$
\boxed{
\text{列出所有數學可能性}
}
$$

---

# 8. 知識集

## 8.1 內部知識

Agent 自身模型參數中的知識：

$$
\mathcal K_t^{\mathrm{param}}.
$$

---

## 8.2 本地研究庫

$$
\mathcal K_t^{\mathrm{local}}.
$$

包括：

- 論文；
- 筆記；
- 已證引理；
- 私有資料；
- 前輪失敗記錄。

---

## 8.3 形式庫

$$
\mathcal K_t^{\mathrm{formal}}.
$$

例如：

- Lean；
- Coq；
- Isabelle；
- HOL；
- 定理資料庫。

---

## 8.4 網路知識

$$
\mathcal K_t^{\mathrm{web}}.
$$

包括：

- 論文；
- 預印本；
- 數學資料庫；
- 討論；
- 軟體文檔；
- 計算結果。

---

## 8.5 總知識

$$
\mathcal K_t
=
\mathcal K_t^{\mathrm{param}}
\cup
\mathcal K_t^{\mathrm{local}}
\cup
\mathcal K_t^{\mathrm{formal}}
\cup
\mathcal K_t^{\mathrm{web}}.
$$

---

# 9. 網路不是查答案，而是知識底空間擴張

## 9.1 缺口生成

若：

$$
T
\not\Rightarrow
M,
$$

Agent 生成：

$$
G_t
=
\operatorname{Gap}(T,M).
$$

---

## 9.2 檢索

$$
R_t
=
\operatorname{Retrieve}(G_t).
$$

---

## 9.3 知識更新

$$
\mathcal K_{t+1}
=
\mathcal K_t
\cup
R_t.
$$

---

## 9.4 動態知識底空間

因此：

$$
\boxed{
\mathcal E_{\mathrm{web}}:
\mathcal K_t
\mapsto
\mathcal K_{t+1}
}
$$

是一個底空間擴張算子。

---

# 10. Phase D：逆向公理回填

對每個：

$$
M_i\in\mathcal M_t,
$$

生成：

$$
\mathcal B(M_i)
=
\{
T_{i1},
T_{i2},
\dots
\}.
$$

再測試：

$$
\bigwedge_jT_{ij}
\Rightarrow
M_i.
$$

---

# 11. Phase E：計算

## 11.1 計算的角色

計算不只用於：

$$
\text{驗證答案}.
$$

更可用於：

- 搜索反例；
- 發現模式；
- 估計參數；
- 比較候補；
- 驗證有限情況；
- 排除錯誤橋樑；
- 提示新不變量。

---

## 11.2 計算結果

定義：

$$
\mathcal C_t
=
\operatorname{Compute}(
\Omega_t
).
$$

---

## 11.3 計算即逼近

若每輪：

$$
\Omega_{t+1}
\subset
\Omega_t,
$$

或：

$$
\mathcal M_{t+1}
$$

更精確，則即使尚未證明：

$$
P,
$$

研究狀態仍可能接近有效路徑。

本文提出：

$$
\boxed{
\text{計算即逼近}
}
$$

作為研究動力學直覺。

---

# 12. Phase F：驗證

驗證層至少包括：

## 12.1 邏輯驗證

$$
T
\Rightarrow
M
\Rightarrow
P?
$$

---

## 12.2 形式驗證

若可形式化：

$$
\operatorname{Check}_{\mathrm{formal}}.
$$

---

## 12.3 數值驗證

對有限域：

$$
\operatorname{Check}_{\mathrm{numeric}}.
$$

---

## 12.4 文獻驗證

檢查：

- 是否已知；
- 是否有反例；
- 是否依賴目標；
- 是否等價於目標。

---

# 13. Phase G：反例搜索

對每個：

$$
M_i,
$$

主動尋找：

$$
w_i
\Rightarrow
\neg M_i.
$$

這一步不可省略。

因為 Agent 若只生成支持，不生成反例，容易造成：

$$
\text{confirmation bias}.
$$

---

# 14. Phase H：失敗分類

定義：

$$
\mathcal F_t
=
\{
F_t^{(1)},
\dots,
F_t^{(m)}
\}.
$$

失敗類別至少包括：

1. false；
2. too strong；
3. too weak；
4. missing node；
5. domain mismatch；
6. circular；
7. equivalent-risk；
8. computationally intractable；
9. semantic explosion；
10. contamination risk。

---

# 15. Phase I：動態更新

研究狀態更新：

$$
\mathcal S_{t+1}
=
\mathcal U(
\mathcal S_t,
\mathcal F_t,
\mathcal C_t,
\mathcal K_{t+1}
).
$$

---

## 15.1 拆分

$$
M
\rightsquigarrow
M_1\land M_2.
$$

---

## 15.2 弱化

$$
M
\rightsquigarrow
M'.
$$

---

## 15.3 強化

$$
M
\rightsquigarrow
M^+.
$$

---

## 15.4 換表示

$$
P(X)
\rightsquigarrow
P'(F(X)).
$$

---

## 15.5 擴域

$$
\mathfrak U_t
\subset
\mathfrak U_{t+1}.
$$

---

# 16. 研究狀態不是靜態檔案，而是動態系統

本文提出：

$$
\boxed{
\mathcal S_{t+1}
=
\mathcal U(
\mathcal S_t
)
}
$$

作為自主數學研究的核心。

若存在某種目標狀態：

$$
\mathcal S^\ast,
$$

則研究可理解為：

$$
\operatorname{dist}(
\mathcal S_t,
\mathcal S^\ast
)
\downarrow.
$$

注意：

$$
\mathcal S^\ast
$$

未必是唯一證明。

可能是：

- 一份證明；
- 一個反例；
- 一個不可判定結果；
- 一個更精確猜想；
- 一組新引理；
- 一個失敗路徑分類。

---

# 17. 理論上的可能效益

以下均為：

$$
\text{待證命題}.
$$

不是已證結果。

---

## 17.1 搜索空間壓縮

若 KCPE 能把：

$$
\mathfrak P
$$

縮為：

$$
\Omega_t,
$$

則可能有：

$$
|\Omega_t|
\ll
|\mathfrak P|.
$$

---

## 17.2 困難重定位

將：

$$
C(P)
$$

重構為：

$$
C(M_1),\dots,C(M_n).
$$

真正困難可能集中在：

$$
M_k.
$$

---

## 17.3 並行化

不同 Agent 可處理：

$$
M_1,\dots,M_n.
$$

因此：

$$
C_{\mathrm{parallel}}
\approx
\max_i C(M_i)
$$

而非：

$$
\sum_iC(M_i).
$$

---

## 17.4 失敗知識累積

若每輪失敗：

$$
F_t
$$

被保存，則未來：

$$
\Omega_{t+1}
$$

可避開重複錯誤。

---

## 17.5 結構保存

錯誤候補可標記：

$$
S
=
\mathrm{StructurallyUseful}.
$$

避免：

$$
\text{錯}
\Rightarrow
\text{全部刪除}.
$$

---

## 17.6 跨域發現

若：

$$
P(X)
$$

長期無法閉合，

Agent 可搜尋：

$$
F:
X
\rightarrow
Y.
$$

將問題轉入另一領域。

---

# 18. 目前尚未證明的效益

本文必須明確承認：

## 18.1 尚未證明搜索空間必然縮小

可能：

$$
|\Omega_{t+1}|
>
|\Omega_t|.
$$

---

## 18.2 尚未證明中介分解必然降低負擔

可能：

$$
\max_i C(M_i)
\ge
C(P).
$$

---

## 18.3 尚未證明 Agent 能穩定生成高質量橋樑

可能大部分：

$$
M_i
$$

都是空殼。

---

## 18.4 尚未證明網路擴張提升研究

可能引入：

- 噪音；
- 錯誤文獻；
- 重複資料；
- 污染。

---

## 18.5 尚未證明反覆循環會收斂

可能：

$$
\mathcal S_t
$$

進入循環。

---

# 19. 可證偽條件

## 19.1 無增益

若大量測試中：

$$
\mathrm{AMRAL}
$$

不優於基線，方法受挑戰。

---

## 19.2 分支爆炸

若：

$$
|\Omega_t|
\rightarrow
\infty
$$

且剪枝無效，KCPE 失敗。

---

## 19.3 回填率過低

若：

$$
R_{\mathrm{fill}}
\approx0,
$$

RAB 失去實用性。

---

## 19.4 循環率過高

若：

$$
R_{\mathrm{circ}}
\rightarrow1,
$$

方法可能退化為目標重述。

---

## 19.5 知識擴張無效

若：

$$
\mathcal K_{t+1}
>
\mathcal K_t
$$

但成功率不升，則底空間擴張假設受挑戰。

---

# 20. 指標

## 20.1 有效橋樑率

$$
R_{\mathrm{bridge}}
=
\frac{
N_{\mathrm{useful}}
}{
N_{\mathrm{generated}}
}.
$$

---

## 20.2 回填率

$$
R_{\mathrm{fill}}
=
\frac{
N_{\mathrm{filled}}
}{
N_{\mathrm{obligations}}
}.
$$

---

## 20.3 反例淘汰率

$$
R_{\mathrm{falsify}}
=
\frac{
N_{\mathrm{refuted}}
}{
N_{\mathrm{tested}}
}.
$$

---

## 20.4 分支壓縮率

$$
R_{\mathrm{compress}}
=
1-
\frac{
|\Omega_{t+1}|
}{
|\Omega_t|
}.
$$

---

## 20.5 新引理率

$$
R_{\mathrm{lemma}}
=
\frac{
N_{\mathrm{new\ usable\ lemmas}}
}{
N_{\mathrm{runs}}
}.
$$

---

## 20.6 工程可觀測性

$$
O_{\mathrm{PE}}.
$$

衡量：

- 候補可見；
- 剪枝可見；
- 失敗可見；
- 依賴可見；
- 重負擔可見。

---

# 21. Agent 架構

## 21.1 Target Agent

負責：

$$
P,\neg P.
$$

---

## 21.2 Bridge Agent

生成：

$$
\mathcal M.
$$

---

## 21.3 Enumeration Agent

生成：

$$
\Omega_t.
$$

---

## 21.4 Retrieval Agent

擴張：

$$
\mathcal K_t.
$$

---

## 21.5 Backfill Agent

尋找：

$$
\mathcal T_i.
$$

---

## 21.6 Compute Agent

執行：

$$
\mathcal C_t.
$$

---

## 21.7 Counterexample Agent

尋找：

$$
\neg M_i.
$$

---

## 21.8 Formal Agent

執行形式驗證。

---

## 21.9 Dependency Auditor

檢查：

$$
P\in\operatorname{Anc}(M_i)?
$$

---

## 21.10 Research Orchestrator

更新：

$$
\mathcal S_{t+1}.
$$

---

# 22. 多 Agent 並行

若：

$$
\mathcal M
=
\{M_1,\dots,M_n\},
$$

則可：

$$
A_i
\mapsto
M_i.
$$

即每個 Agent 處理不同橋樑。

---

## 22.1 橫向並行

不同橋樑。

---

## 22.2 縱向並行

同一橋樑的不同回填。

---

## 22.3 對抗並行

一個 Agent 證明：

$$
M.
$$

另一個 Agent 搜索：

$$
\neg M.
$$

---

# 23. 計算工具接入

AMRAL 可調用：

- Python；
- Rust；
- SAT；
- SMT；
- CAS；
- Lean；
- Coq；
- 圖論庫；
- 數值分析；
- 高性能計算；
- 資料庫。

---

# 24. 證明超圖

定義：

$$
\mathfrak G_t
=
(V_t,\mathcal E_t).
$$

節點：

$$
V_t
=
\{
P,
M_i,
T_j,
W_k
\}.
$$

超邊：

$$
\{T_1,T_2\}
\rightarrow
M.
$$

---

# 25. 研究記憶

每輪保存：

$$
\mathcal H_t
=
(
\mathcal S_0,
\dots,
\mathcal S_t
).
$$

因此 Agent 不應重複：

$$
\text{已知失敗路線}.
$$

---

# 26. 知識污染

自主 Agent 搜網路時會遇到：

$$
\text{solution leakage}.
$$

因此需要：

$$
A_{\mathrm{contam}}.
$$

---

## 26.1 污染類型

1. 直接答案；
2. 標準證明；
3. 關鍵引理名稱；
4. 作者提示；
5. 領域提示。

---

## 26.2 控制

真正盲測應：

- 隱去名稱；
- 隱去作者；
- 預註冊；
- 哈希承諾；
- 事後揭示。

---

# 27. 安全邊界

## 27.1 未證橋樑不得升格

$$
M_i[\mathrm P]
$$

不得寫成：

$$
M_i[\mathrm F].
$$

---

## 27.2 有限計算不得冒充無限證明

$$
N<\infty
$$

驗證不等於：

$$
\forall N.
$$

---

## 27.3 網路來源不得自動視為真

$$
\operatorname{Retrieved}
\not\Rightarrow
\operatorname{Valid}.
$$

---

# 28. 初步理論命題

以下均未證。

---

## 命題 A：動態逼近命題

存在某些問題類，使：

$$
\operatorname{dist}(
\mathcal S_{t+1},
\mathcal S^\ast
)
<
\operatorname{dist}(
\mathcal S_t,
\mathcal S^\ast
).
$$

---

## 命題 B：知識條件化優勢命題

KCPE 在某些問題類上優於無條件候補生成。

---

## 命題 C：失敗累積優勢命題

保存：

$$
\mathcal F_{<t}
$$

可降低重複搜索。

---

## 命題 D：對抗代理優勢命題

證明 Agent 與反證 Agent 並行，可提高錯誤候補淘汰率。

---

## 命題 E：底空間擴張命題

針對明確 Gap 的檢索：

$$
G_t
\rightarrow
\mathcal K_{t+1}
$$

比無目標瀏覽更有效。

---

# 29. 與普通自動定理證明的差異

普通 ATP 主要：

$$
\text{Fixed theory}
+
\text{Goal}
\rightarrow
\text{Search}.
$$

AMRAL：

$$
\text{Goal}
\rightarrow
\text{Intermediate generation}
\rightarrow
\text{Knowledge expansion}
\rightarrow
\text{Computation}
\rightarrow
\text{Search reconstruction}.
$$

---

# 30. 與普通 Agent 的差異

普通 Agent 可能：

$$
\text{Plan}
\rightarrow
\text{Tool}
\rightarrow
\text{Answer}.
$$

AMRAL：

$$
\text{Research state}
\rightarrow
\text{Persistent iteration}.
$$

---

# 31. 理論上的長期願景

若未來有效，AMRAL 可能形成：

$$
\text{自主研究循環}
$$

而非：

$$
\text{單輪問答}.
$$

Agent 可以：

1. 維持長期問題；
2. 累積失敗；
3. 自動查新文獻；
4. 自動重跑計算；
5. 自動更新中介命題；
6. 自動提交形式驗證。

---

# 32. 目前真正缺少的部分

## 32.1 真正實作

尚未完成：

$$
\mathrm{AMRAL}_{\mathrm{full}}.
$$

---

## 32.2 大規模基準

尚未有：

$$
N\gg1
$$

的定理集合。

---

## 32.3 語義寬度估計器

尚未成熟。

---

## 32.4 證明負擔估計器

$$
C(P)
$$

仍難量化。

---

## 32.5 收斂理論

尚未證明：

$$
\mathcal S_t
\rightarrow
\mathcal S^\ast.
$$

---

# 33. 建議的第一版實作

## Stage 1

單 Agent：

$$
\mathrm{RIITG}
+
\mathrm{RAB}.
$$

---

## Stage 2

加入：

$$
\mathrm{KCPE}.
$$

---

## Stage 3

加入：

- web retrieval；
- formal library；
- Python；
- SAT/SMT。

---

## Stage 4

多 Agent。

---

## Stage 5

持續研究記憶。

---

# 34. 偽代碼

```text
INPUT:
    target proposition P
    initial knowledge K0
    semantic window W
    compute budget B
    iteration limit T

STATE:
    S0 = {
        P,
        K0,
        M = {},
        Supports = {},
        Candidates = {},
        Failures = {},
        Computations = {},
        DependencyGraph = {}
    }

FOR t in 0..T:

    1. Normalize P
    2. Construct not-P
    3. Generate bridge propositions M_t
    4. Score semantic width
    5. Build candidate space Omega_t
    6. Search internal knowledge
    7. Detect knowledge gaps
    8. Retrieve external knowledge for gaps
    9. Update K_t
    10. Generate backfill supports
    11. Run computations
    12. Search counterexamples
    13. Verify implications
    14. Build proof hypergraph
    15. Detect circularity
    16. Classify failures
    17. Prune candidates
    18. Split / weaken / strengthen bridges
    19. Update research state S_{t+1}

    IF proof closed:
        return proof + audit trail

    IF counterexample found:
        return disproof + audit trail

    IF semantic explosion:
        return structured failure

OUTPUT:
    best research state
    unresolved gaps
    candidate lemmas
    failed routes
    computation logs
```

---

# 35. 預期輸出

AMRAL 不應只輸出：

$$
\text{Proof}
$$

或：

$$
\text{No Proof}.
$$

而應輸出：

1. 當前最佳路線；
2. 未填橋樑；
3. 反例；
4. 失敗原因；
5. 候補引理；
6. 文獻來源；
7. 計算結果；
8. 依賴圖；
9. 污染風險；
10. 下一輪建議。

---

# 36. 本文最核心的理論判斷

本文提出：

$$
\boxed{
\text{數學研究}
\neq
\text{一次性證明輸出}
}
$$

更可能是：

$$
\boxed{
\text{研究狀態的持續更新}
}
$$

因此：

$$
\mathcal S_t
\rightarrow
\mathcal S_{t+1}
$$

才是自主研究 Agent 的核心。

---

# 37. 結論

本文提出一套尚未完成一般性證明、尚未完成完整實作的自主數學研究 Agent 初步架構。

其核心由三部分組成：

$$
\boxed{
\mathrm{RIITG}
}
$$

負責由結果反向生成中介命題；

$$
\boxed{
\mathrm{RAB}
}
$$

負責將暫態橋樑降格並回填；

$$
\boxed{
\mathrm{KCPE}
}
$$

負責在知識、失敗、語義窗口與計算預算條件下執行局部類窮舉。

三者共同形成：

$$
\boxed{
\mathrm{AMRAL}
}
$$

即自主數學研究代理循環。

完整動態為：

$$
\text{Analyze}
\rightarrow
\text{Generate}
\rightarrow
\text{Enumerate}
\rightarrow
\text{Retrieve}
\rightarrow
\text{Backfill}
\rightarrow
\text{Compute}
\rightarrow
\text{Verify}
\rightarrow
\text{Falsify}
\rightarrow
\text{Update}.
$$

本文不宣稱：

$$
\mathrm{AMRAL}
$$

已被證明有效。

本文只主張：

> 從理論結構、現有 Agent 能力、搜尋、檢索、計算、形式驗證與多代理並行等條件看，這種架構具有可實作可能性。

真正需要後續證明與實驗的是：

1. 是否能穩定降低搜索空間；
2. 是否能提高有效中介命題率；
3. 是否能降低重複失敗；
4. 是否能提高新引理發現率；
5. 是否能在低污染盲測中優於基線。

因此本文的最終定位是：

$$
\boxed{
\text{可實作的理論候選架構}
}
$$

而不是：

$$
\boxed{
\text{已證明的通用數學研究系統}
}
$$

但若未來其中部分命題得到支持，則自主數學 Agent 可能不再只是：

> 解一道題。

而是：

> 持續研究一個問題，直到問題本身、知識底空間、候補證明圖與計算結果共同演化。

這也是本文真正提出的長期方向：

$$
\boxed{
\text{研究即動態計算；
計算即持續逼近。}
}
$$

---

# 附錄 A：最小形式化

## A.1 研究狀態

$$
\mathcal S_t
=
(
P_t,
\mathcal K_t,
\mathcal M_t,
\mathcal T_t,
\Omega_t,
\mathcal F_t,
\mathcal C_t,
\mathcal D_t
).
$$

---

## A.2 RIITG

$$
P_t
\rightsquigarrow
\mathcal M_t.
$$

---

## A.3 RAB

$$
\mathcal T_t
\Rightarrow
\mathcal M_t.
$$

---

## A.4 KCPE

$$
\Omega_t
=
\Omega(
P_t,
\mathcal K_t,
\mathcal F_{<t},
W_{\mathrm{sem}},
B_t
).
$$

---

## A.5 知識擴張

$$
\mathcal K_{t+1}
=
\mathcal K_t
\cup
\operatorname{Retrieve}(
G_t
).
$$

---

## A.6 狀態更新

$$
\mathcal S_{t+1}
=
\mathcal U(
\mathcal S_t,
\mathcal F_t,
\mathcal C_t,
\mathcal K_{t+1}
).
$$

---

# 附錄 B：方法狀態標記

- **K**：Known
- **P**：Provisional
- **C**：Conjectural
- **F**：Filled
- **R**：Refuted
- **S**：Structurally Useful
- **E**：Equivalent Risk
- **D**：Dependency Risk
- **X**：Contamination Risk

---

# 附錄 C：研究誠信聲明

1. 本文架構尚未證明具有一般性增益。
2. 本文尚未完成完整 AMRAL 系統實作。
3. 本文不宣稱自主 Agent 已能獨立解決開放數學難題。
4. 本文所有效益均為待驗證命題。
5. 任何未證橋樑不得被寫成定理。
6. 任何網路資料不得自動視為真。
7. 任何有限計算不得冒充無限證明。
8. 任何新穎性主張都需事後文獻審計。
9. 若未來大規模實驗不支持本方法，應公開保留失敗結果。
10. 本文定位為初版草稿與可實作研究架構。

---

# 附錄 D：與前三篇的關係

本文可視為前述三篇研究的第四層延伸：

1. **錯誤生成保存層**  
   將錯誤中的結構性價值保留。

2. **證明工程層**  
   建立 RIITG 與 RAB。

3. **實驗審計層**  
   建立準盲測、污染控制與證明工程可觀測性。

4. **自主研究代理層**  
   本文提出 AMRAL 與 KCPE，將方法變成可反覆執行的 Agent 研究循環。