上海人工智慧實驗室訪問學者、大灣區大學教授許地生團隊，依託書生科學多模態大模型S2（書生-S2），以人機協同方式完成了三維Ghys猜想的證明。北京大學董彬教授、劉若川院士團隊隨後利用自主開發的SHEAF框架對證明進行形式化驗證，全部四個主定理通過Lean檢驗。相關論文已釋出在預印本平台arXiv，形式化程式碼在GitHub公開。

Ghys猜想由法國數學家艾蒂安·吉斯於1995年提出，核心問題是：混沌的動力系統行為能否決定幾何上的分類。通俗理解，若一個封閉、無邊界且區域性遵循複數運算規則的“世界”中存在某種既混沌又完全規則的運動，那麼這個世界的形狀就只能是由簡單規則反覆拼接的高度規整結構，例如復環面，其運動本質上只是平移、旋轉或縮放。該猜想被動力系統領域專家公認為最重要的長期公開問題之一，也是檢驗數學推理能力的試金石。

許地生長期研究這一猜想，曾與其導師、菲爾茲獎得主阿圖爾·阿維拉合作探索三維情形但未形成有效證明思路，此後與學生張潔松合作取得部分弱相關結果，刊發於《歐洲數學會雜誌》。2026年3月，許地生成為上海AI實驗室訪問學者，雙方組建聯合團隊並搭建面向數學研究的Harness系統。8月，內部迭代成型的書生-S2具備大規模遞迴推理與靈活人機互動能力，針對三維Ghys猜想的首輪推理即產出400頁推導報告。

技術層面，團隊堅持“通專融合”路線，在大規模科學知識預訓練基礎上構造研究級後訓練資料，並突破非同步長程推理強化學習訓練方法，解決誤差指數級累積、長期狀態維護與自我糾錯等難題，還將Harness帶來的能力提升反向蒸餾回模型。在IMO-Proof、AdvancedMathBench等基準上，書生-S2整體領先現有開源模型，部分指標超越Gemini 3.1 Pro等閉源模型。

攻關過程中，書生-S2先後完成7批接續推演，問題圖從15個節點擴充套件到389個，輸出總量達上千頁嚴密推導，並生成數十種全新論證思路。研究人員負責把握方向、判斷思路價值並給出直覺建議，模型承擔海量繁瑣推導，雙方通過多輪對話迭代推進。值得注意的是，動力系統專家謝俊逸教授此前曾用GPT-6嘗試該題未找到證明方案，這從側面印證了書生-S2在本次探索中的獨特價值。

驗證環節，北大團隊完成論文全部四個主定理的形式化驗證。骨幹成員姜傑東、吳彬介紹，整個過程僅約5天，峰值併發達100個智慧體，產出約55萬行Lean程式碼。形式化難度不僅來自數學本身——自然語言證明常依賴讀者補全條件，形式化須落實為計算機可檢查的完整證明——還因動力系統領域原有形式化基礎設施不足，此次補充了大量基礎設施。團隊使用SHEAF框架，將命題、定義及依賴關係組織成從目標定理逐層延伸到基礎定理庫的有向無環圖，把大規模形式化任務分解為可檢查的步驟。

北大數學團隊早在2021年便佈局AI for Math方向，搭建了覆蓋高難度評測集FATE、數學知識檢索Matlas/LeanSearch、自動推理與形式化驗證Rethlas/Archon/Danus/Iteris的完整技術鏈條，其AI系統曾攻克安德森猜想，近期還獨立完成龐加萊猜想的形式化驗證。

本項研究的意義還在於驗證了一種新科研範式：將專家直覺系統性接入機器求解迴路，形成“系統探索—專家判斷—成果積累—反饋修正”的閉環。這一範式可複製到更多“搜尋空間巨大而專家稀缺”的基礎研究領域。接下來，團隊將把跑通的能力閉環封裝為書生·端硯科學發現平台可複用的數學驗證模組，並以三維Ghys猜想為起點，將推理能力擴充套件至數學結構同源的其他學科，形成“突破—封裝—複用—再突破”的自進化飛輪。