中國人工智能框架獨立解決並正式驗證了一個持續超過十年未解的交換代數開放問題。研究人員表示，這套中國 AI 系統幾乎完全自主運作，從頭到尾無需人類介入。領導該項目的 15 人團隊由北京大學研究員主導，針對 2014 年由前愛荷華大學數學教授 Dan Anderson 提出的猜想。Anderson 已於 2022 年以 73 歲之齡逝世。
雙代理架構
系統核心採用雙代理設計，配對兩個專門組件。首先是 Rethlas，作為非正式推理代理，模擬人類數學家工作方式，包括探索證明策略、產生候選解法，並透過自訂定理搜尋引擎 Matlas，從數十年數學文獻中檢索相關結果，甚至涵蓋問題周邊領域。其次是 Archon，負責正式驗證，配備自家搜尋引擎 LeanSearch。它從 Rethlas 提取候選證明，將其轉譯為 Lean 4 正式程式語言，用於機器可驗證的數學證明。
Archon 會將任務拆解成步驟、精煉並自動建構證明。兩個代理共同彌補 AI 在數學領域的長期挑戰：自然語言推理靈活但不精確，與正式驗證嚴謹卻脆弱之間的斷層。 中國 AI 系統另一優勢在於跨領域應用數學技巧，通常需不同數學分支專家合作。研究員指出，Rethlas 的成功主要歸功 Matlas，能發現並套用跨域定理，引導系統得出可行證明。Archon 則獨立填補非正式論證缺口，這需相當程度的數學推理能力。
團隊亦測試 Archon 於 FirstProof 基準，這是由學術數學家提出的 10 個研究級問題集合。在 Google Aletheia 系統失敗的兩個案例中，Archon 產生完整形式化證明，一個完全自主，另一個僅需一個自然語言提示。 該論文尚未經同行評審，未宣稱框架能解決所有數學開放問題，但證明 AI 結合推理與驗證的新研究途徑可產生可靠、可查證結果。
團隊已將形式化結果及 Rethlas 與 Archon 程式碼上傳 GitHub，以 FrenzyMath 名義公開。AI 應用於高等數學的競爭日益激烈。今年稍早，Google DeepMind 的 Aletheia 解決了 Erdős 猜想資料庫中的四個開放問題。OpenAI 亦展示正式證明能力，但兩系統均需人類監督。北京大學團隊框架似已減少或消除此需求。
該中國 AI 成就首見於 arXiv 預印本論文。
