上海AI實驗室“書生-S2”大模型進入前沿數學研究流程：助力三維Ghys猜想證明並通過形式化驗證

上海人工智能實驗室（上海AI實驗室）訪問學者、大灣區大學教授許地生團隊依託書生科學多模態大模型S2（書生-S2），基於“通專融合”技術路徑，通過人機協同完成了三維Ghys猜想證明。北京大學董彬教授、劉若川院士團隊利用其開發的SHEAF框架對本次證明完成形式化驗證，驗證了這一工作的正確性。有業內人士認為，這標誌著中國科學家首次用中國大模型攻克世界級數學難題。“Ghys猜想”由法國數學家艾蒂安·吉斯（Étienne Ghys）於1995年提出，猜測每一個緊緻複流形上的全純Anosov系統，都雙全純共軛於某個復infra-冪零流形上的全純仿射自同構。

該問題兼具理論難度與學科標誌性價值，被動力系統領域數學專家公認為該領域最重要的長期公開問題之一，是檢驗數學推理能力的一塊試金石。相關論文已在預印本平臺（arXiv）發佈，其形式化代碼也在Github平臺公開。Ghys猜想，為混沌系統尋找“底層代碼”1995年，法國數學家艾蒂安·吉斯（Étienne Ghys）提出Ghys猜想，其核心是：混沌的動力系統行為的存在是否能決定幾何上的分類。這是復動力系統領域的一個重要難題。如果這一猜想成立，混亂的動力學軌跡的問題就能被“化歸”成簡潔、規整的標準代數模型。如何理解Ghys猜想？可以想象在一個封閉有限、沒有邊界、每一小塊都遵守複數運算規則的“世界”。

對Anosov系統，可藉助揉麵類比：按壓、延展、摺疊麵糰，部分方向被拉伸，部分方向被壓縮。拉伸效應會讓初始緊鄰的點快速分離——初始條件微小差異，會帶來截然不同的演化結果。Ghys猜想說，只要存在這樣一種“既像揉麵又完全規則”的運動，那麼這個“世界”就只能是一種由簡單規則反覆拼接、像晶體格子一樣高度規整的形狀。例如復環面：換個視角看，這個運動本質上就是這個“世界”的簡單平移、旋轉或縮放。也就是說，運動方式太混沌，會反過來決定世界只能長成什麼形狀。

2026年國際數學家大會45分鐘報告人，北京大學北京國際數學研究中心謝俊逸教授評價：“Ghys猜想的難點在於其對應的實（數）版本的類似斷言仍是著名的完全公開的難題，複數的情形問題變得更加剛性，是復動力系統剛性現象研究中的重要問題，非常困難”。大灣區大學教授許地生長期深耕該猜想的研究，曾與其導師、菲爾茲獎得主阿圖爾·阿維拉（Avila）教授合作研究三維情形，但未形成有效的證明思路；此後他與其學生張潔松博士合作在三維情形下取得Ghys猜想的部分弱相關結果，相關成果刊發於數學頂級期刊《歐洲數學會雜誌》（JEMS）。7批接續推演、389個節點，人機協同取得關鍵突破 “科學發現是對智能的終極考驗。

”上海人工智能實驗室主任、首席科學家周伯文作出過一個判斷：問題越古老、越基礎，AI提效的空間越大——AI參與攻關的單克隆抗體、蛋白質摺疊，以及至今懸而未決的千禧年難題納維-斯托克斯方程，都符合這條規律。三維Ghys猜想正是這類基礎性難題中的一個。2026年3月，許地生教授成為上海AI實驗室訪問學者，他與上海AI實驗室的科研協作由此走向更深、更緊密的階段，雙方組建聯合團隊，並同步搭建了面向數學研究場景的Harness系統。許地生教授結合數學科研經驗，精準指出模型與系統的能力短板；依託真實前沿數學研究命題，驅動系統完成多輪迭代打磨。

8月，內部迭代成型的書生-S2及配套系統，具備大規模遞歸推理能力，同時擁有高靈活性的人機交互能力，在複雜數學命題的處理能力上實現質的躍升。其中，針對三維Ghys猜想的首輪推理，書生-S2就產出了400頁的推導報告。在訓練策略層面，科研團隊堅持“通專融合”技術路線，在大規模科學知識預訓練夯實模型底座基礎上，精心構造研究級後訓練數據，包括大規模來自數學論文的難題和可靠的校驗方案，提升模型在研究級數學上的專業性、嚴謹性和規範性。

在訓練算法層面，科研團隊突破了異步長程推理強化學習訓練方法，在可驗證獎勵下破解了誤差指數級累積、長期狀態維護、自我糾錯等一系列根本性難題；團隊還同時研發了將Harness帶來的能力提升反向蒸餾回模型的自進化算法，在大量超出模型直推能力邊界的高難度問題上持續獲得有效監督信號，推進模型能力的自主提升。在IMO-Proof、AdvancedMathBench等強調長程嚴謹推理的競賽數學與高等數學基準上，書生-S2整體領先現有開源模型，並在部分指標上超越Gemini 3.1 Pro等頂尖閉源模型，躋身全球長程推理能力最強的開源模型之列。

至此，書生-S2的基模能力已具備輔助科研團隊攻關研究級數學問題的基本水平，但距離真正破解世界級難題，還需要更上一層樓。團隊認為，突破的關鍵在於更緊密的人機協同：書生-S2及配套系統發揮長鏈條大規模推演的優勢，鋪開多條支線同步嘗試、拆解複雜命題、猜想不同的思路，把海量繁瑣的推導工作承接下來，每一輪迭代給出海量嘗試結果；研究人員則負責把握大方向，判斷哪些思路值得深挖、哪些路徑是死衚衕、給出一些直覺建議，作為系統下一輪迭代的指令。二者並非單方獨立推導，而是人機協同，通過多輪對話和反饋，在緊密互動中進行迭代。圖中展示了系統的多輪交互過程及各輪交互中的遞歸求解結構。

其中，邊僅表示子問題的分解關係，不表示上下文依賴關係；每個節點均可訪問時序上先於該節點的全部全局上下文。在AI給出的首輪探索基礎上，數學家許地生與張潔松敏銳抓住關鍵突破口，持續給模型反饋、校準探索方向，引導模型向有價值的思路深耕。攻關過程中，書生-S2先後完成7批接續推演，問題圖從15個節點擴展到389個，輸出總量達上千頁的嚴密推導，同時生成數十種全新論證思路，成功助力團隊破解這一世界級數學難題，得到該方向國際前沿學者“思考深度遠超預期”的評價。有意思的是，在論文上傳預印本網站arXiv之前，前文提及的動力系統專家謝俊逸教授也曾用GPT-6嘗試挑戰這道題，並沒有找到證明方案。

“這不僅印證了書生-S2在本次前沿數學探索中的獨特價值，同時也傳遞出一個信號——中國的大模型同樣有能力站上前沿數學的賽場，助力世界級難題的攻關。” 北大團隊給出專業形式化驗證AI助力產出的成果是否經得起驗證？北京大學董彬教授、劉若川院士團隊完成了本次論文全部四個主定理的形式化驗證，證明已通過Lean檢驗。Lean作為交互式定理證明系統，能對形式化證明進行嚴格邏輯檢查。北大團隊骨幹成員姜傑東、吳彬介紹，整個過程僅約5天，峰值併發達100個智能體，產出約55萬行Lean代碼，展現出極大的並行規模與極快的驗證速度。專家確認形式化陳述與論文主定理語義一致，Lean驗證據此確保其嚴格正確性。

形式化的難度首先來自數學本身：自然語言證明常依賴讀者的數學知識補全條件與推理，形式化則須將其落實為計算機可檢查的完整證明。論文引用的結果若未進入基礎定理庫，還需補充形式化證明，或尋找利用已有結果的替代路線。尤其動力系統領域原有形式化基礎設施不足，此次工作補充了大量基礎設施，覆蓋論文依賴的眾多文獻結果。對研究級數學而言，這些工作涉及定義的準確表達、證明結構的拆解和數學工具的選擇；大量智能體並行時，還須確保各部分的定義、陳述和依賴相互銜接，局部證明才能組成完整證明鏈。

為組織這一過程，北大團隊使用了自主開發的SHEAF框架：多個智能體將論文中的命題、定義及依賴關係組織成一張從目標定理逐層延伸到基礎定理庫的有向無環圖；模型在框架下參與命題分解與形式化證明構建，團隊圍繞該圖編排工作，跟蹤各節點的陳述、證明與剪枝狀態，將大規模形式化任務分解為相互銜接、可檢查的步驟。早在 2021 年大模型尚未問世之時，北京大學北京國際數學研究中心董彬教授團隊便敏銳洞察到人工智能將重塑數學研究範式。

北大數學團隊是國際上最早佈局 AI for Math 方向的研究團隊之一，搭建起覆蓋高難度評測集（FATE）、大規模數學知識檢索（Matlas/LeanSearch）、自動推理與形式化驗證（Rethlas/Archon/Danus/Iteris）的完整技術鏈條；其開發的 AI 系統成功攻克安德森猜想這一公開數學難題，實現國內首例、同時也是國際上首個由高校團隊主導，依託人工智能自主突破重大數學猜想的成果。近期，團隊還獨立完成了龐加萊猜想的形式化驗證工作。從單一難題破解，到科研基礎設施本項研究的意義還在於驗證了一種新的科研範式。

傳統數學研究依賴個體天才的漫長摸索，而本次攻關將專家直覺系統性接入機器求解迴路，形成“系統探索—專家判斷—成果積累—反饋修正”的閉環。這一範式可複製推廣至更多“搜索空間巨大而專家稀缺”的基礎研究領域，實現更多“從0到1”的原始創新突破。接下來，依託本次研究跑通的完整能力閉環，團隊將進一步封裝為書生·端硯科學發現平臺可複用的數學驗證模塊，供後續科學問題研究直接調用。同時，以三維Ghys猜想的突破作為起點，上海AI實驗室將沉澱的推理能力擴展應用於數學結構同源的其他學科；取得新突破後，再將新推理能力封裝回端硯平臺複用，與更多學科結合尋求下一輪突破，形成“突破—封裝—複用—再突破”的自進化飛輪。

也將持續跟進這一方向的最新進展。