中國大模型首破世界級數學難題：書生-S2 助力證明三維 Ghys 猜想
一個 1995 年提出的剛性猜想
10 月 15 日，上海人工智慧實驗室釋出訊息：困擾數學界三十餘年的三維 Ghys（吉斯）猜想迎來破解。上海人工智慧實驗室訪問學者、大灣區大學教授許地生團隊依託書生科學多模態大模型 S2（書生-S2），通過人機協同完成了這項證明；北京大學董彬教授、劉若川院士團隊利用其開發的 SHEAF 框架完成形式化驗證。相關論文已在預印本平臺 arXiv 釋出，形式化程式碼在 GitHub 公開。實驗室稱，這是中國科學家首次用中國大模型攻克世界級數學難題。
猜想說了什麼？Ghys 猜想由法國數學家 Étienne Ghys 於 1995 年提出，猜測每一個緊緻複流形上的全純 Anosov 系統，都雙全純共軛於某個復 infra-冪零流形上的全純仿射自同構。實驗室給出的直觀是這樣：想像一個封閉有限、沒有邊界、每一小塊都遵守複數運算規則的「世界」，如果它上面存在一種「既像揉麵又完全規則」的運動，那麼這個世界只能是由簡單規則反覆拼接、像晶體格子一樣高度規整的形狀，比如復環面；而這個運動本質上只是這個世界裡的平移、旋轉或縮放。
為什麼這件事很難？2026 年國際數學家大會 45 分鐘報告人、北京大學謝俊逸教授的評語是：Ghys 猜想的難點在於其對應的實數版本的類似斷言，至今仍是著名的完全公開難題，而複數情形變得更加剛性，是復動力系統剛性現象研究中的重要問題，非常困難。許地生曾與導師、菲爾茲獎得主阿圖爾·阿維拉合作研究三維情形，但未形成有效的證明思路；此後他與張潔松在三維情形取得部分弱相關結果，相關成果刊發於數學期刊《歐洲數學會雜誌》（JEMS）。
起點是一場奧數 AI 測試
突破的起點，是書生大模型在 2025 年全國中學生數學奧林匹克（CMO）決賽中的表現。2025 年，中國數學會中學數學競賽委員會在 CMO 首次設立 AI 測試，共邀請三家國產大模型參與，與人類選手在相同時長內完成答題，並由官方組織以相同標準閱卷評分。其中書生-S1 取得 102 分，不僅在參評大模型中排名第一，更遠超 78 分的金牌線。
閱卷專家對書生-S1 答卷的印象是「答案表達方式非常接近人類」，其中一種解法被描述為巧妙的新解法，在參賽學生的答卷裡沒有出現過。許地生長期從事動力系統、譜理論、分形幾何與 AI4Math 等方向研究，注意到這套模型在數學上的潛力；而拿到 CMO 成績後的上海人工智慧實驗室，也在探索把模型能力從競賽級推向難度更高的研究級數學。雙方目標不謀而合，2026 年初正式啟動模型訓練合作研究。
聯合團隊同步搭建了面向數學研究場景的 Harness 系統。許地生結合自己的科研經驗，指出模型與系統的能力短板，並以真實的前沿數學命題驅動系統完成多輪迭代打磨。迭代成型的書生-S2 及配套系統具備大規模遞迴推理能力，同時擁有高靈活性的人機互動能力，在複雜數學命題的處理能力上實現了明顯躍升。
上千頁推導，判斷由人來做
攻關過程中，針對三維 Ghys 猜想的首輪推理，書生-S2 就產出了 400 頁的推導報告。從 2026 年 8 月起，模型從多個角度對猜想開展試探，前後完成 7 批接續推演，問題圖從 15 個節點擴充套件到 389 個，輸出總量達千頁的嚴密推導，同時生成數十種全新的論證思路，其中不乏新穎構想。
分工是清晰的。模型發揮長鏈條大規模推演的優勢，鋪開多條支線同步嘗試、拆解複雜命題、把海量繁瑣的推導工作承接下來，每一輪迭代給出大量嘗試結果；研究人員則負責把握大方向，判斷哪些思路值得深挖、哪些路徑是死衚衕，並給出直覺性的建議，作為系統下一輪迭代的指令。完整的證明鏈條不是模型獨立推出的，而是人與模型多輪對話、彼此啟發、一次次試錯後拼起來的。論文作者在 arXiv 中宣告：使用了 Intern-S2 協助發展數學思想與論證，但由作者獨立核驗全部數學論證並承擔責任。論文由許地生的學生、現就職於瑞典皇家理工學院的張潔松博士完成並整理。論文題為《Codimension-one holomorphic Anosov diffeomorphisms》（餘維一的全純 Anosov 微分同胚），其核心定理證明的是 Ghys 猜想的餘維一情形，並特別推出復維數三的情形。
這裡需要寫準一句話：這次解決的是餘維一情形（因而覆蓋復三維情形），並不等於整個 Ghys 猜想已被完全解決。論文本身也討論了高餘維情形中存在的障礙，例如某些高維全純 Anosov 系統的穩定與不穩定分佈可能並不全純，因此一般的高餘維版本不能據此宣稱已經完成。把「破解三維 Ghys 猜想」與「證明整個 Ghys 猜想」區分開，才是對這項工作最準確的表述。
還有一段有意思的旁證：在論文上傳到 arXiv 之前，謝俊逸收到了團隊送來的論文。他聽說這是由國內模型做出的，特意用 GPT-6 進行了測試，但並未解決該問題。實驗室把這件事視為書生-S2 在這次前沿數學探索中獨特價值的旁證，也當作一個訊號——中國的大模型同樣有能力站上前沿數學的賽場。
形式化驗證，以及一臺「飛輪」
AI 產出的成果能否經得起檢驗？北京大學董彬、劉若川團隊完成了本次論文全部四個主定理的形式化驗證，證明已通過 Lean 檢驗。Lean 是互動式定理證明系統，能對形式化證明進行嚴格的邏輯檢查。北大團隊骨幹成員姜傑東、吳彬介紹，整個過程僅約 5 天，峰值併發達 100 個智慧體，產出約 55 萬行 Lean 程式碼，展現出極大的並行規模與極快的驗證速度。專家確認，形式化陳述與論文主定理語義一致。
形式化的難度首先來自數學本身：自然語言的證明常常依賴讀者用既有知識補全條件與推理，形式化則必須把這些落實為計算機可以檢查的完整證明。論文引用的結果如果沒有進入基礎定理庫，還要補充形式化證明，或尋找利用已有結果的替代路線。動力系統領域原有的形式化基礎設施不足，這次工作補充了大量基礎設施。為組織這一過程，北大團隊使用了自主開發的 SHEAF 框架，把論文中的命題、定義及依賴關係組織成一張從目標定理逐層延伸到基礎定理庫的有向無環圖，再圍繞這張圖編排工作、跟蹤各節點的陳述、證明與剪枝狀態。
邊界仍要說清楚。Lean 檢驗的是形式化程式碼中的邏輯正確性：它能確保所陳述的定理被嚴格證明，但不能自動保證論文裡每一處自然語言表述、建模選擇與定理形式化都沒有偏差；而 arXiv 上的論文是預印本，也還不等於經過期刊同行評議的正式發表版本。形式化驗證與同行評議是兩種不同性質的檢驗，缺一不可。
這項研究的意義不止於一個難題被解決，而在於它驗證了一種新的研究範式：傳統數學研究依賴個體天才的漫長摸索，而這次攻關把專家直覺系統性地接入了機器求解迴路，形成「系統探索—專家判斷—成果積累—反饋修正」的閉環。實驗室認為，這套範式可以複製推廣到更多「搜尋空間巨大而專家稀缺」的基礎研究領域。接下來，團隊打算把這次跑通的完整能力閉環封裝為書生·端硯科學發現平臺可複用的數學驗證模組，供後續科學問題研究直接呼叫；同時以三維 Ghys 猜想的突破為起點，把沉澱的推理能力擴充套件應用到數學結構同源的其他學科，取得新突破後再把新能力封裝回平臺複用，形成「突破—封裝—複用—再突破」的自進化飛輪。這套說法能否兌現，要看下一次別的學科問題上的表現。