據(jù)研發(fā)團隊介紹，中國一個人工智能框架已自主解決了美國數(shù)學家在十多年前提出的一個公開問題——安德森猜想。

前不久，北京大學牽頭的研究團隊發(fā)了一篇預印本論文，論文稱，通過整合數(shù)十年的數(shù)學文獻，他們的AI框架彌合了自然語言推理與機器形式驗證之間的鴻溝，成功解決了美國數(shù)學家丹·安德森早在2014年就提出的一個懸而未決的問題，并在幾乎無需人類干預的情況下自動完成了證明的形式化。

其實這些年隨著大語言模型發(fā)展，AI搞數(shù)學已經(jīng)不是新鮮事了，比如谷歌的Gemini Deep Think，都已是能在最頂尖的青年數(shù)學競賽國際奧數(shù)上拿到金牌水平了。但要說AI能完全自己搞定研究級別的數(shù)學難題，之前還真不行。

這是因為數(shù)學證明最講究的就是百分之百嚴謹，哪怕是大專家寫的證明，都可能藏著你看不出來的小漏洞，大語言模型本身又容易“胡編亂造”，結果根本靠不住，所以此前就算是利用AI執(zhí)行數(shù)學計算，都得大量靠人類盯著，沒法實現(xiàn)全自動。

這次中國團隊的思路就特別妙，直接讓兩個AI智能體分工干活。第一個叫Rethlas，專門“想思路”，它就像人類數(shù)學家一樣，借助數(shù)學定理搜索引擎Matlas探索解題策略，先攢出一個像模像樣的候選證明草稿;第二個叫Archon，專門“把草稿變嚴謹”，它會用專門的定理搜索工具，把非正式證明轉換成可以被機器完全驗證的正式項目。

他們拿這套方法去試安德森那道交換代數(shù)里的問題——交換代數(shù)是現(xiàn)代代數(shù)幾何、數(shù)論的基礎。AI自己給了一個反例的非正式證明，推翻了原來問題的前提，隨后僅用80小時的智能體運行時間，就把整個證明的形式化驗證全做完了。整個過程中，人類只干了一件事：幫AI下了幾個它無法自行獲取的付費文件，連“這個證明對不對”這種數(shù)學判斷，都完全沒用人類出手。

研究人員寫道：“總的來說，我們的結果表明，對于真正的數(shù)學公開問題，非正式推理智能體和形式智能體可以有效協(xié)作?！笔聦嵣?，AI和數(shù)學本來就是互相成就的，數(shù)學為AI發(fā)展提供理論基礎，而AI工具則可以加速數(shù)學研究本身。