自主數學研究代理循環

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

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

重要聲明

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

本文目前不主張：

\mathrm{RIITG}+\mathrm{RAB}

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

本文也不主張：

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

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

本文真正提出的是：

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

因此，本文應被視為：

自主數學研究方法論與 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.

候選角色至少包括：

表示橋樑；
排他橋樑；
不變量橋樑；
正性橋樑；
壓縮橋樑；
局部—全域橋樑；
閉包橋樑；
反例證人橋樑；
計算可判定橋樑；
跨域映射橋樑。

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)} \}.

失敗類別至少包括：

false；
too strong；
too weak；
missing node；
domain mismatch；
circular；
equivalent-risk；
computationally intractable；
semantic explosion；
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 污染類型

直接答案；
標準證明；
關鍵引理名稱；
作者提示；
領域提示。

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 可以：

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

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. 偽代碼

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}.

而應輸出：

當前最佳路線；
未填橋樑；
反例；
失敗原因；
候補引理；
文獻來源；
計算結果；
依賴圖；
污染風險；
下一輪建議。

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 能力、搜尋、檢索、計算、形式驗證與多代理並行等條件看，這種架構具有可實作可能性。

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

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

因此本文的最終定位是：

\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：研究誠信聲明

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

附錄 D：與前三篇的關係

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

錯誤生成保存層
將錯誤中的結構性價值保留。
證明工程層
建立 RIITG 與 RAB。
實驗審計層
建立準盲測、污染控制與證明工程可觀測性。
自主研究代理層
本文提出 AMRAL 與 KCPE，將方法變成可反覆執行的 Agent 研究循環。

自主數學研究代理循環_結果誘導中介定理生成_逆向公理回填與知識條件化類窮舉_v0.1

自主數學研究代理循環

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

重要聲明

摘要

1. 導論

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

1.2 本文真正的研究對象

2. 前置方法

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

2.2 逆向公理回填法

2.3 完整方向

3. 從方法到 Agent

3.1 單次方法不足

3.2 研究狀態

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

5. Phase A：目標分析

5.1 正規化

5.2 生成否定

5.3 生成反例形狀

6. Phase B：中介命題生成

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

7.1 為何不是暴力窮舉

7.2 候補空間

7.3 類窮舉的真正含義

8. 知識集

8.1 內部知識

8.2 本地研究庫

8.3 形式庫

8.4 網路知識

8.5 總知識

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

9.1 缺口生成

9.2 檢索

9.3 知識更新

9.4 動態知識底空間

10. Phase D：逆向公理回填

11. Phase E：計算

11.1 計算的角色

11.2 計算結果

11.3 計算即逼近

12. Phase F：驗證

12.1 邏輯驗證

12.2 形式驗證

12.3 數值驗證

12.4 文獻驗證

13. Phase G：反例搜索

14. Phase H：失敗分類

15. Phase I：動態更新

15.1 拆分

15.2 弱化

15.3 強化

15.4 換表示

15.5 擴域

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

17. 理論上的可能效益

17.1 搜索空間壓縮

17.2 困難重定位

17.3 並行化

17.4 失敗知識累積

17.5 結構保存

17.6 跨域發現

18. 目前尚未證明的效益

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

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

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

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

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

19. 可證偽條件

19.1 無增益

19.2 分支爆炸

19.3 回填率過低

19.4 循環率過高

19.5 知識擴張無效

20. 指標

20.1 有效橋樑率

20.2 回填率

20.3 反例淘汰率

20.4 分支壓縮率

20.5 新引理率