7月6日，中國科學院數學與系統科學研究院（以下簡稱數學院）發布基于大語言模型的數學研究智能體“數學機械化智能體（MechMath Agent Team，簡稱MMAT）”，該智能體搭建起了覆蓋數學研究全流程的研究框架，是數學家的全新智能研究助手，這標志著我國大模型驅動的定理證明技術實現前沿科研級突破。
經過兩個月內部測試驗證，MMAT獨立或與數學家交互攻克了代數計算理論、微分代數、數論領域8項長期公開問題，比如稀疏多項式計算復雜性與最優算法、廣義艾里算子等價問題，以及BSD猜想重要研究內容等。其中2項問題由MMAT全自動獨立解決，6項問題的核心關鍵引理由MMAT完成證明。同時，MMAT還給出了2項難題證明過程的形式化驗證，驗證結果嚴謹可靠。
研發團隊負責人、數學院研究員高小山介紹，MMAT采用分層多智能體協同的核心設計思路，構建了系統、完整的大模型推理框架。他們首先將數學家的研究思路和環節進行模塊化，打造出二十個左右具備專項能力的子智能體；其次，針對不同類型的數學問題，系統可智能調度各子智能體分工協作，自主生成求解方案、完成問題解答，并通過多層迭代機制完成結果核驗。
在框架的基礎上，研究團隊融合子智能體與外部工具，構建了MMAT的三個智能體，實現自主規劃定理證明全流程、可自動生成Lean形式化代碼，并進行自然語言與形式化語義對齊，以及描繪面向研究對象的數學知識圖譜。
相較于傳統數學大模型和簡易數學智能體，這一設計很大程度上突破了只能給出單一證明、缺乏全局規劃、易出現邏輯幻覺、難以開展復雜課題研究等局限，大幅提升了人工智能參與數學研究的能力。
高小山表示，MMAT具備數學知識覆蓋面廣、問題求解能力突出、邏輯輸出穩定性強、無明顯幻覺問題等顯著優勢。同時他坦言，當前，智能體在面對超高難度數學難題時，無法一次性輸出完整嚴謹證明的局限，數學家在研究問題提煉、證明準確性校驗、創新思路開拓、全新數學概念引入等環節，依然發揮著不可替代的核心主導作用。
中國科學院院士、數學院研究員田野認為，數學機械化智能體整合大語言模型、知識管理、自然語言證明、形式化驗證、符號計算、人機協同等多項技術，構建起了覆蓋數學研究全過程的一體化智能系統。這一成果代表了全新數學研究路徑，推動人工智能從單一模型輸出模式，升級為可審計、可復用、可積累的人機協同科研平臺。
中國科學院院士、數學院院長張平指出，數學機械化智能體不只是單項技術的創新突破，更有望推動數學研究范式的深層次變革。展望未來，數學研究將形成全新協同模式：由人類數學家提出科研問題、把控研究方向，大模型開展探索推演與定理證明，數學機械化智能體完成大規模精準計算，形式化系統筑牢科研嚴謹性底線，四方協同聯動，推動人工智能輔助數學研究走得更遠、更扎實。