據研發團隊介紹，中國一個人工智慧框架已自主解決了美國數學家在十多年前提出的一個公開問題——安德森猜想。
前不久，北京大學牽頭的研究團隊發了一篇預印本論文，論文稱，通過整合數十年的數學文獻，他們的AI框架彌合了自然語言推理與機器形式驗證之間的鴻溝，成功解決了美國數學家丹·安德森早在2014年就提出的一個懸而未決的問題，並在幾乎無需人類干預的情況下自動完成了證明的形式化。
其實這些年隨著大語言模型發展，AI搞數學已經不是新鮮事了，比如谷歌的Gemini Deep Think，都已是能在最頂尖的青年數學競賽國際奧數上拿到金牌水平了。但要說AI能完全自己搞定研究級別的數學難題，之前還真不行。
這是因為數學證明最講究的就是百分之百嚴謹，哪怕是大專家寫的證明，都可能藏著你看不出來的小漏洞，大語言模型本身又容易「胡編亂造」，結果根本靠不住，所以此前就算是利用AI執行數學計算，都得大量靠人類盯著，沒法實現全自動。
這次中國團隊的思路就特別妙，直接讓兩個AI智能體分工幹活。第一個叫Rethlas，專門「想思路」，它就像人類數學家一樣，藉助數學定理搜索引擎Matlas探索解題策略，先攢出一個像模像樣的候選證明草稿；第二個叫Archon，專門「把草稿變嚴謹」，它會用專門的定理搜索工具，把非正式證明轉換成可以被機器完全驗證的正式項目。
他們拿這套方法去試安德森那道交換代數里的問題——交換代數是現代代數幾何、數論的基礎。AI自己給了一個反例的非正式證明，推翻了原來問題的前提，隨後僅用80小時的智能體運行時間，就把整個證明的形式化驗證全做完了。整個過程中，人類只幹了一件事：幫AI下了幾個它無法自行獲取的付費文件，連「這個證明對不對」這種數學判斷，都完全沒用人類出手。
研究人員寫道：「總的來說，我們的結果表明，對於真正的數學公開問題，非正式推理智能體和形式智能體可以有效協作。」事實上，AI和數學本來就是互相成就的，數學為AI發展提供理論基礎，而AI工具則可以加速數學研究本身。
