1995 年提出的數學問題取得新進展
一項於 1995 年提出的數學猜想，在數學家與上海人工智慧實驗室 Intern-S2 模型合作後，獲得涵蓋複數維度三的證明。隨後，北京大學團隊將論文的四項主要定理轉化為由 Lean 驗證的證明；Lean 是一套旨在驗證數學推理的電腦系統。
目錄
上海人工智慧實驗室於 2026 年 10 月 15 日宣布這項成果，並指出研究團隊由徐迪生領導。徐迪生是大灣區大學教授，也是該實驗室的訪問學者。研究論文《餘維一全純 Anosov 微分同胚》的唯一作者，是瑞典皇家理工學院的張傑松。
這項成果解決了法國數學家 Étienne Ghys 猜想中的餘維一情形，包括複數維度三的情形。它關乎運動與形狀之間一種引人注目的關係：能夠支撐某種混沌運動的空間，本身是否必須具有高度有序的數學結構。
Intern-S2 透過與研究人員反覆交流，協助發展思路與論證。張傑松在 AI 使用聲明中表示，他已獨立驗證所有數學內容。這項合作結合了機器探索、人類判斷，以及另一套獨立的形式化驗證流程。
實驗室稱，這是中國 AI 模型首次協助解決如此高難度的數學問題。具體成果是一項分類定理，另有公開的預印本與正式發布的形式化程式碼。
這項證明如何描述運動與形狀
Ghys 猜想屬於複動力系統領域，研究數學系統的座標遵循複數規則變化時，系統會如何演變。複數由兩個實數分量組成，因此複數維度三在局部相當於六個實數維度。這個研究背景比一般物體在房間中移動更加抽象。
Anosov 系統具有精確的拉伸與壓縮組合。在反覆運動下，某些方向收縮，另一些方向則擴張。相近的起始點可能迅速分離，因此即使每一步都遵循精確規則，仍會產生混沌行為。
可以把它想成反覆拉伸並摺疊形狀的過程。不過，本文研究的數學系統有更嚴格的限制：拉伸與收縮必須符合一致的條件，運動也必須保留複數座標所提供的結構。
Ghys 提出，緊緻複流形上的這類系統，應該能以標準的代數形式描述。流形是指在小範圍內看起來簡單、整體形狀卻可能複雜的空間。在此情境下，緊緻性是一種數學條件，可避免空間無限延伸。
張傑松的定理指出，緊緻連通複流形上的每個餘維一全純 Anosov 微分同胚，都與複環面上的雙曲自同構雙全純共軛。簡單來說，透過保留複結構的可逆座標變換，便能將這種運動轉化為一個非常規則空間上的標準代數變換。
複環面可以透過識別複數空間中相差一個週期晶格元素的點來構造。這項成果的核心在於，複雜的動力系統竟迫使空間具有如此有序的幾何描述。
為何精確界定範圍很重要
這篇論文探討的是餘維一情形。對這類系統而言，代表收縮或擴張部分之一的複數維度為一。定理一般性地涵蓋這個受限的系統族，並解決複數維度三時的猜想。
Ghys 更廣泛的猜想涉及範圍更廣的複流形上的全純 Anosov 系統，並以稱為複 infra-nilmanifold 的空間上的標準代數模型描述這些系統。張傑松的結果則為本文研究的情形提供一個特別嚴謹的答案：複環面與雙曲自同構。
對研究這個問題的數學家來說，這項定理將問題從找出未知的空間與運動，轉變為研究標準模型。座標變換可將原始系統連結到該模型，同時保留複幾何結構。
徐迪生多年來一直研究這個問題。他先前曾與前指導教授、菲爾茲獎得主 Artur Avila 一起探討維度三的情形。徐迪生與張傑松後來取得相關的部分成果，並刊登於《歐洲數學學會期刊》。這項新研究延續了他們對同一數學問題的長期投入。
從奧林匹亞競賽到研究合作
Intern-S2 的參與，延續了 Intern-S1 在 2025 年中國數學奧林匹亞競賽中的早期成果。中國數學會負責中學數學競賽的委員會當年舉辦 AI 測試，邀請三款中國模型在與人類參賽者相同的時間限制內解題。
按照相同評分標準，Intern-S1 得分 102 分，在三款參賽模型中排名第一。金牌門檻為 78 分，因此它高出 24 分，約高出 31%。
徐迪生認為這個模型系列有機會應用於數學研究；上海人工智慧實驗室則希望從競賽題目進一步挑戰尚未解決的問題。雙方於 2026 年初展開合作，並打造一套稱為 Harness 的軟體系統，用來組織模型的工作及其與研究人員的交流。
主要階段如下：
- 1995 年：Étienne Ghys 提出這項猜想。
- 2025 年：Intern-S1 在中國數學奧林匹亞競賽 AI 測試中獲得 102 分。
- 2026 年初：徐迪生與上海人工智慧實驗室展開模型訓練合作。
- 2026 年 3 月：徐迪生出任實驗室訪問學者。
- 2026 年 8 月：內部開發的 Intern-S2 版本及其支援系統，達到可用於密集數學探索的階段。
- 9 月 29 日：張傑松的論文發布於 arXiv，並於 10 月 13 日更新版本。
- 2026 年 10 月 15 日：公開宣布這項成果。
數學家如何引導 AI
Intern-S2 首次探索這個問題時，產生了一份約 400 頁的推導報告。徐迪生邀請曾是他學生、目前在瑞典皇家理工學院從事博士後研究的張傑松加入，擔任訪問學者。張傑松從博士研究期間便開始關注 Ghys 猜想。
徐迪生與張傑松檢視模型提出的構想，找出有發展潛力的切入點，並提供回饋引導後續探索。機器負責推進不同的推理路線並產生論證；數學家則決定哪些方向值得深入研究，並協助組織出最終證明。
實驗室表示，模型分七批持續推理。在此過程中，模型的問題圖從 15 個節點擴增至 389 個，累積輸出約達千頁，並包含數十種提議的解法。
問題圖是呈現較小數學任務及其關聯的圖示。某個節點可能代表一項中間主張，另一個節點則代表證明該主張所需的結果。據稱節點數量的增長，顯示系統以多深入的程度拆解並探索這個問題。
張傑松的 AI 使用聲明直接說明了誰對最終的數學成果負責：Intern-S2 的內部版本透過多輪對話協助發展構想與論證，而他本人獨立檢查了數學內容。他也在論文中感謝徐迪生持續參與討論。
支援軟體的貢獻
上海人工智慧實驗室為模型搭配軟體，協助管理長串推理過程與反覆的人類回饋。系統能將困難問題拆解為較小任務、探索多個方向，並交由研究人員評估結果。
訓練方法結合了廣泛的科學知識與研究數學相關資料，包括取自數學論文的難題，以及檢查解答的方法。實驗室也介紹了運用可驗證獎勵的強化學習，也就是以成功且可檢查的推理作為訓練訊號。
研究人員隨後運用支援系統累積的經驗來改進模型。實際目標是在長期研究過程中維持有效進展，包括追蹤中間結果，並隨著新論證發展而修正錯誤。
實驗室也提到 IMO-Proof 和 AdvancedMathBench 的成果，這兩項評測聚焦於數學推理。至於 Ghys 猜想專案，最詳盡的系統運作證據，來自一連串大量推導、專家回饋、完成的論文，以及後續的形式化驗證。
北京大學如何驗證證明
由董彬與劉若川領導的北京大學團隊，運用 SHEAF 框架將張傑松論文中的四項主要定理全部形式化。這項工作也涵蓋了論證所依據的 Ghys 相關結果。
形式化是將數學定義、假設與推理轉譯成電腦能夠檢查的語言。一般論文可以仰賴受過訓練的讀者自行補足熟悉的推理步驟；Lean 則要求以精確陳述和允許的邏輯運算表達這些步驟。
團隊成員江傑東與吳彬表示，這項工作耗時約五天，最多有 100 個 AI 代理平行運作，產生約 55 萬行 Lean 程式碼。專家也檢查了形式化陳述是否符合論文主要定理的數學意義。
SHEAF 將任務組織成一個由定義、命題及相依關係構成的有向圖。如此一來，不同代理便能處理彼此相關的部分，團隊也能追蹤哪些陳述已經證明，哪些仍待處理。
形式化工作不只是轉譯最終論證。現有的形式化數學函式庫缺少部分動力系統的輔助結果，因此團隊必須補上基礎，或設法運用既有結果，再將各部分串接成完整的論證鏈。
這篇論文已以 arXiv 預印本形式公開，形式化程式碼也已發布於 GitHub。公告並未說明論文是否已在期刊發表或通過同儕審查。
兩個階段為何相輔相成
Intern-S2 與 SHEAF 的用途不同。前者協助尋找數學構想與論證，後者則協助建構可由 Lean 檢查的形式化證明。人類數學家引導探索、檢查所得的數學內容，並評估形式化陳述是否表達了原定理的意義。
這項工作的規模清楚呈現兩者的分工：約千頁的探索輸出，成為研究論文的素材；接著，驗證流程產生約 55 萬行形式化程式碼。每個階段都將成果轉化為適合不同任務的形式。
對未來的研究人員而言，公開論文呈現數學論證，公開程式碼則記錄形式化證明的結構。形式化過程中新增的支援定義與結果，也可能成為同一領域後續研究的起點。
下一步是建立可重複使用的驗證模組
上海人工智慧實驗室計畫將這套工作流程包裝成數學驗證模組，供 Intern 杜延科學發現平台使用。目標是讓後續研究專案重複運用模型探索、專家回饋與形式化檢查的組合。
實驗室也計畫將這項專案發展出的推理能力，應用於具有相關數學結構的其他學科。其構想是建立一個循環：解決研究問題、將有用方法製作成可重複使用的軟體，再應用於另一項研究。
對徐迪生而言，這項成果透過大灣區大學、上海人工智慧實驗室、瑞典皇家理工學院與北京大學的合作，延續了他長期投入的研究方向。對更廣大的數學界來說，這項工作不僅帶來新的分類結果，也具體展示了 AI 如何在人類引導下參與研究。
重點整理
- 這項新證明解決了 Ghys 猜想的餘維一情形，包括複數維度三。
- 張傑松是研究論文的唯一作者，並表示自己已獨立驗證所有數學內容。
- 徐迪生與張傑松透過反覆探索與回饋，引導 Intern-S2。
- 模型的問題圖從 15 個節點增至 389 個，推導內容約千頁。
- 北京大學的 SHEAF 框架協助將四項主要定理及其支援結果形式化為 Lean 證明。
- 據稱驗證工作耗時約五天，產生約 55 萬行程式碼。
- 實驗室計畫將這套工作流程發展成可重複使用的數學驗證模組。
