上海AI實驗室書生-S2協助完成三維Ghys猜想證明，北大以Lean完成形式化驗證

上海人工智能實验室訪問學者、大灣區大學教授許地生團隊依託書生科學多模態大模型S2（書生-S2），以「通專融合」技術路徑，透過人機協同完成三維Ghys猜想證明。北京大學董彬教授、劉若川院士團隊使用其開發的SHEAF框架完成形式化驗證。Ghys猜想由法國數學家Étienne Ghys於1995年提出，被動力系統領域專家視為最重要的長期公開問題之一。據報導，相關論文已發布於arXiv，形式化程式碼公開於GitHub；業內人士認為這是中國科學家首次以中國大模型攻克世界級數學難題，此說法來源尚未獨立證實。 過程方面，許地生與張潔松此前已在三維情形取得部分弱相關結果，並發表於《歐洲數學會雜誌》（JEMS）。2026年3月許地生成為上海AI實驗室訪問學者後雙方組建聯合團隊，並搭建面向數學研究的Harness系統。書生-S2首輪推理即產出400頁推導報告；攻關期間共進行7批接續推演，問題圖由15個節點擴展至389個，輸出總量上千頁，並生成數十種新論證思路。研究人員負責判斷方向，模型負責大量分支嘗試，雙方透過多輪互動迭代。 形式化驗證方面，北大團隊完成論文全部四個主定理的Lean驗證並通過檢查，耗時約5天，峰值並行100個智能體，產出約55萬行Lean程式碼。專家確認形式化陳述與論文主定理語義一致。由於動力系統領域原有形式化基礎設施不足，此次工作另補充了大量基礎設施。 另有報導指出，北京大學謝俊逸教授在論文發布前曾以GPT-6嘗試此題，但未找到證明方案，該說法亦未經其他來源佐證。