AI4Math團隊

團隊概況

AI4Math團隊是北京大學董彬課題組與合作者組建的研究團隊，隸屬於北京大學北京國際數學研究中心（BICMR）。團隊於2023年正式組建，核心成員包括劉若川、肖梁、文再文、董彬等教授。團隊成員來自代數與數論、最佳化、機器學習與人工智慧等多學科背景。

主要成就

2026年4月，AI4Math團隊使用其構建的自動化AI框架，解決了交換代數中的開放問題Anderson猜想，並在Lean 4中完成了約19000行的形式化驗證。這是國內首次利用AI框架處理此類代數問題並實現大規模形式化驗證。田剛院士提及了該成果。該框架能夠完成同等規模的形式化工作。

技術框架

AI4Math團隊搭建的雙智慧型體協作框架由自然語言推理智慧型體Rethlas和形式化驗證智慧型體Archon組成。該框架基於現有基座模型構建。研究中，Rethlas通過團隊自研的Matlas自然語言語義檢索系統，從上千萬條數學陳述中定位關鍵結果，例如在解決Anderson猜想時，Rethlas定位到Jensen(2006)的一個技術性結果，並據此構造反例。

Archon負責將證明轉化為Lean 4代碼，能發現初始方案存在的邏輯漏洞，重新設計形式化證明的技術路線。當所需數學概念於Lean形式化數學庫中未收錄時，Archon能找到等價替代路徑。該框架完成的代碼覆蓋6篇外部論文關鍵結果，完成約19000行代碼的形式化驗證。Archon已開源。

研究背景

團隊的研究工作基於三年的技術積累與跨學科協作。2022年初，在劉若川和肖梁兩位教授引薦下，董彬教授課題組開始與時任香港中文大學教授何旭華合作，利用機器學習方法分析一類代數幾何對象，相關成果於2024年發表在《Peking Mathematical Journal》上。團隊初期選定的研究目標之一，即交換代數中的Anderson猜想，正是由肖梁教授為團隊選定。

工具與基礎設施

為支撐AI數學推理，AI4Math團隊打造了雙引擎檢索架構。LeanSearch允許用戶使用自然語言描述需求進行語義檢索，在Lean官方社區中提供使用，其API日均調用量約為8000次。Matlas覆蓋了上千萬條數學陳述，支持命題級的語義檢索。

支持與資助

團隊在AI4Math方向與至知創新研究院(iQuest Research)在算力、資源與技術方面有緊密合作，並得到新基石科學基金會對基礎研究的長期資助。