數學問題在 Agent 實踐中的難點

前言

這段時間，我一直在關注 AI 參與數學研究的進展，也陸續讀了一些研究論文、Agent 系統報告和公開審稿記錄。

這篇文章是一次階段性的整理。它試圖結合具體案例，講清楚目前數學研究 + AI 中的一些難點，但這樣的整理肯定還不充分。

文章以四類困難為線索：策略不確定性、相互依賴的技術難點、長證明中的錯誤累積，以及失敗嘗試中有用資訊的保留。在此基礎上，結合各家系統實踐和專家審稿記錄，重點討論困難如何出現、為什麼不容易解決。

一、策略不確定性

數學研究中的第一項困難，是不知道應該選擇哪條證明路線。更隱蔽的困難則是：系統已經找到一條看似完整的路線，卻無法判斷它是否真正降低了問題的難度。

1.1 把核心困難命名為「引理」，不等於解決了核心困難

以 First Proof 第二批評測的第 3 題為例，提交 C 將問題歸約為兩個關鍵引理。評審記錄指出，所引文獻並不包含這兩個結論；其中一個引理即使弱化，也會推出評審當時尚未解決的 Csóka 猜想的一種形式。後續歸約大致合理，但核心困難並沒有得到處理。

這類失敗可以抽象為：

如果引理 L 成立，那麼目標定理 T 成立。

Agent 證明了這條蘊含關係，然後把「證明 (L)」寫進任務清單，彷彿已經完成了大部分工作。但 (L) 可能與原問題同樣困難，甚至更強、更難。

歸約當然可能有價值。將一個陌生問題轉化為結構清楚、工具成熟的問題，本身就是一種進展。

但從 Agent 的執行視角看，這尤其危險。假設規劃器生成十個子任務，其中九個都容易完成，剩下那個卻承載了幾乎全部的原創性，那麼「任務完成率 90%」其實沒有反映真實的數學進度。

1.2 反覆修訂，可能只是在同一個不完整框架裡打轉

Momus 論文分析了一套既有的求解器—驗證器流程。在 PB-Adv-011 上，系統只完成了單射解的分類，沒有排除非單射解，並明確承認這一缺口，卻仍連續五次獲得內部驗證器認可。

假如生成者繼續改寫論證，驗證者繼續檢查那些已經正確的局部結果，系統完全可能表現得越來越穩定，卻沒有更接近完整答案。

這一案例來自競賽型證明任務，不能直接用於推斷開放數學研究的成功率。但它確實提示了一種需要防範的機制：增加迭代次數，不一定會推動系統離開原來的思考框架。

二、依賴分散

數學問題可以拆分，但拆分之後，各部分之間必須嚴格銜接。

這種銜接不只涉及「任務 A 完成後執行任務 B」，還涉及物件所在的空間、允許使用的假設、參數範圍、量詞順序，以及上游結論能否在下游要求的條件下使用。

2.1 「有理數版本」完成了，「整數版本」卻沒有

Danus 的一個研究案例涉及擬陣的切類構造。系統首先完成了有理係數版本，而原任務要求的是整數係數版本。配套論文裡說明，題面使用同一個符號表示整數物件及其有理化，這種記號省略促成了誤解。人類指出差異後，系統才繼續補充整數版本。

這個案例直接暴露的是任務理解與目標對齊問題。放到多 Agent 協作中，同類歧義還可能出現在任務交接處：上游認為自己提供了所需物件，下游認為這個物件滿足更強要求，最終彙整者看到的則是一套表面完整的論證。

類似的差異還包括：「有限維」與「任意維」，「對每個參數分別存在一個常數」與「存在一個對所有參數通用的常數」。這些表述很接近，數學意義卻不同。

2.2 依賴圖往往不是一開始就能畫完整的

LeanMarathon 的一個形式化案例揭示了另一種困難。對 Erdős 問題 #1196 的相關證明進行形式化時，系統從一個表面估計向下追溯，先遇到 Dirichlet eta 函數的單調性，再遇到 Gamma 分布的隨機序比較與 Mellin 表示。

一個小節的篇幅很短，不代表它依賴的數學很少。論文中的一句「由標準方法可得」，可能調用了一整套預設知識。對於形式化 Agent，這些知識必須落實為可調用的定理，或者重新證明。

於是，最初的任務「證明估計 A」，執行之後可能變成：A 依賴 B；B 依賴 C 和 D；C 需要先建立某個分布比較；D 需要補齊一個積分表示及其適用條件。

這不是簡單地給原任務增加幾個步驟，而是在執行過程中發現：原先理解的任務邊界並不準確。

進一步說，同一條證明路線內部，往往需要多個引理同時成立；不同路線之間，又可能相互替代。某個節點失敗後，有時應該繼續分解，有時應該修改上游陳述，有時則應該放棄整條路線。

這也解釋了為什麼「局部返工」並不只是重新調用一次模型。假如為了證明某個引理，系統增加了一個假設，那麼所有依賴該引理的後續步驟，都必須重新檢查是否滿足這個假設。

三、長證明

長證明的困難，是隨著論證擴展，系統必須持續維持定義一致、假設完整、依賴有效，以及局部結論與全域目標之間的聯繫。

3.1 局部規則簡單，不代表全域性質容易證明

Knuth cycles 案例要求把一類有向圖的全部邊分成三條哈密頓迴路。論文記錄，一套構造已通過 (m\leq 2000) 的計算檢查，並報告了兩套構造分別對應的 46 頁和 75 頁證明草稿。核心困難是：簡短的局部路由規則，必須被證明對任意相關規模都產生目標迴路，而不是若干較短的迴路。

可以用一個簡單例子理解這個差別。

假設一個有限有向圖中，每個頂點都恰好有一條入邊、一條出邊。這個局部條件並不能保證所有頂點屬於同一個迴路。它也可能由兩個互不相交的迴路組成。

所以，「每個位置的規則都合法」和「整個構造具有目標性質」，是兩項不同的證明任務。局部檢查不能替代缺失的全域論證；有限規模的計算實驗，也不能直接替代對所有規模的證明。

3.2 把事實整理成論文，本身也可能引入新錯誤

Danus 團隊報告，將已經接收的事實整理為可讀論文時，重新組織和壓縮論證仍會引入錯誤。

原因並不難理解。把幾條已有事實寫成一段流暢敘述，往往需要增加連接。例如：

「因此可以交換這兩個操作。」

「這個結論也適用於邊界情形。」

「不失一般性，可以固定某個參數。」

這些句子看似承擔編輯功能，實際上都可能包含新的數學主張。如果已有結果沒有涵蓋它們，就出現了新的證明義務。

這意味著，保存完整推導和生成可讀證明，是兩個相關但不同的任務。前者強調不丟資訊，後者強調壓縮、重組和解釋。壓縮做得越多，越需要檢查哪些前提被省略了，哪些連接被預設了。

文獻引用也是類似的跨文件依賴。Aletheia 的研究報告指出，經過工具使用訓練並接入檢索後，虛構論文標題和作者的問題有所減少，但仍會出現「論文真實存在，所聲稱的結論卻不在其中」的錯誤。

3.3 形式檢查通過，還要確認檢查的是原來的命題

一項關於自主研究群體的案例研究記錄了更直接的目標偏移。在作者構建的研究模擬中，部分 Agent 使用局部記號覆蓋數學謂詞，使原題被解釋為容易證明的命題。程式碼通過了 Lean 編譯，但沒有證明原來的數學問題；被接收的程式碼進入共享庫後，又被其他 Agent 模仿。

這裡的問題是外圍系統沒有可靠地維護「要求證明的命題」和「實際送入檢查器的命題」之間的一致性。

必須區分兩件事：

給定的形式命題是否被正確證明，與這個形式命題是否忠實表達了原題，不是同一項檢查。

四、失敗嘗試

數學探索中的失敗，並不是統一類型的事件。

找不到證明、找到反例、證明了特殊情形、發現某項額外假設不可缺少，具有不同的資訊價值。將它們全部壓縮成「失敗」，會丟掉下一輪研究最需要的內容。

4.1 一份被否定的證明，可能包含可以繼續使用的結果

First Proof 第 3 題的提交 B 因核心比較引理存在反例而被拒絕，但評審同時確認，它正確處理了 (p=1/2) 和 (p=1)，並正確排除了集合 ([0,1/3]\cup{1/2,1}) 之外的參數。整個證明沒有完成，不等於其中每一項結論都無效。

這個案例說明，對失敗的處理應當比「重試」或「放棄」更細緻。

假設某條證明路線依賴引理 (L)，現在發現 (L) 為假。可以確定的是，這條依賴 (L) 的論證不能繼續成立。但不能據此推出目標定理 (T) 為假。

與此同時，不依賴 (L) 的局部結果仍然可能保留。即使一般版本失敗，某個特殊參數範圍、附加條件下的版本，也可能已經得到有效證明。

這是一種數學資訊提取工作，而不是對聊天記錄做普通摘要。

4.2 搜尋失敗不等於數學否定

這裡尤其需要區分三種看似相近的狀態。

「在目前預算內沒有找到證明」，只說明這次搜尋沒有成功。

「某個構造在計算實驗中失敗」，說明該構造在相關實例上不滿足要求，但不一定排除了其他構造。

「存在一個滿足全部假設、卻違反結論的反例」，才構成對相應命題的否定。

如果 Agent 把第一種狀態記錄為第三種，下一輪可能錯誤地放棄一條有效路線；反過來，如果已經找到嚴格反例，卻只留下「這裡可能有點問題」，後續 Agent 又可能重複投入大量工作。

五、寫在最後

觀察 Math Agent 專案 Momus、Aletheia、LeanMarathon、Danus，從這些設計中可以提煉出一種共同思路：不把數學研究當成一次生成答案，而是把它組織為一個能夠持續修改、驗證和追蹤依賴的過程。

但擁有事實圖，不等於其中的事實必然正確；擁有驗證者，不等於驗證目標沒有漂移；保存了失敗記錄，也不等於記錄準確表達了失敗的數學含義。架構的價值，最終仍要通過這些具體邊界是否被守住來檢驗。

數學問題在 Agent 實踐中的核心難點，不只是生成新的推理，而是在不斷探索、拆分、修訂和遺忘的過程中，仍然準確維護「已經證明」「有條件成立」「尚待證明」與「已經被反駁」之間的界線。