一個懸置三十年的猜想、一個中國模型，與一份經機器驗證的證明

一個懸置三十年的猜想、一個中國模型，與一份經機器驗證的證明

10月15日，Shanghai AI Laboratory（上海人工智慧實驗室）宣布，一支研究團隊證明了 Ghys 猜想的三維情形——這是動力系統中一個自1995年起懸而未決的公開問題。相關工作由該實驗室自有的 Intern-S2 模型推進，最終完成的證明由 Peking University（北京大學）的團隊在 Lean 中完成形式化驗證。

其意義不只是一道難題被攻克。更在於這次發布圍繞的是過程而非某個數字：模型給出推導，研究者決定把注意力投向哪幾條進攻路線，證明助手則逐步核驗每一個環節。這套組合正是業界過去兩年反覆承諾的東西，如今它終於配上了一篇論文。

這個猜想問的是什麼

Étienne Ghys 於1995年提出這個問題。大致來說，它問的是：混沌動力系統的行為能否決定其幾何分類——換個說法，就是運動能否告訴你它所在空間的形狀。

被解決的並不是那個一般性問題。團隊證明的是餘維一情形，也就是三維情形，它在三十年間一直懸而未決。這一區分對誠實理解該聲明很重要：完整猜想仍然更寬泛，但那個此前難倒所有人的特定情形，如今已經落定。

第一輪就產出了四百頁

這次協作的具體機制比結果本身更有意思，因為它展示了人機科研在每一分鐘裡實際上是什麼樣子。

Intern-S2 對該問題的首次探索產出了一份約400頁的推演報告。那不是答案，而是一堆候選推理，其中一些有用、一些沒用——當你讓模型去思考一個真正未解的問題，而不是回憶已知的東西時，得到的正是這種形態的產出。

此後，工作又經過七輪持續推理。問題圖——即子命題及其相互依賴關係的圖譜——從15個節點擴展到389個。累計產出約達一千頁，涵蓋數十種不同思路。在每一個階段，數學家都做了模型自己做不到的事：審視這些提案，判斷哪些突破口有希望，並引導下一輪方向。

實驗室訪問學者、Greater Bay University 教授 Xu Disheng，以及自博士階段起便一直追蹤該猜想的博士後研究者 Zhang Jiesong，提供了這種判斷力。Zhang 的論文於9月29日發布到 arXiv，10月13日修訂，是一篇單作者論文，並附有 AI 使用聲明：模型透過多輪對話協助發展了思路與論證，而他對數學部分做了獨立核驗。

讓它不止是一個故事的部分

關於 AI 解決數學問題的說法很廉價。這一次之所以有分量，在於證明被形式化了。

由 Bin Dong 和 Ruochuan Liu 領銜的 Peking University 團隊，用其自有的 SHEAF 框架，把四個主要定理，以及論證所依賴的 Ghys 支撐性結果，全部加以形式化。形式化意味著把定義、假設和推理翻譯成電腦可以檢查的語言——寫作者的每一步論證都必須被明確寫出，而不能留給受過訓練的讀者去補全。

這項工作大約花了五天，最多時有100個 agent 並行工作，產出約55萬行 Lean 程式碼。Lean 是一個互動式定理證明器。它不在乎誰有多自信。它檢查邏輯，要麼接受這份證明，要麼不接受。

SHEAF 把任務組織成由定義、命題和依賴關係構成的有向圖，使不同的 agent 可以處理相互連接的片段，同時團隊追蹤哪些陳述已有證明、哪些仍需要。這是一種真正新型的分工方式；該框架還必須修補現有動力系統形式化庫中的空缺，因為這份證明所需的工具鏈當時根本還不存在。

人與模型，各司其職

實驗室描述的這套分工值得照單全收，因為它對雙方都不是那種好聽的說辭。

模型負責檢索文獻、把命題拆解成小塊、並行探索證明分支、檢查邏輯步驟，並快速測試大量想法。人負責定方向、判斷哪些路徑值得追求，並做出決定下一輪精力投向何處的取捨。

這兩半截然不同。模型的貢獻在規模與耐力：它能同時記住幾十條死巷而不氣餒。人的貢獻是品味，也就是能從一百頁看似合理的推理中，看出哪三段才是關鍵的能力。

這裡還附著一則中國媒體大加渲染的趣聞。據報導，一位動力系統專家在聽說國內某模型解決了該問題後，出於好奇把同樣的問題拋給了 GPT-6，結果它沒能做到。狹義地看，這只是兩個系統在同一個問題上的比較，說明不了太多。若作為競爭態勢的訊號來讀，它正是那種會驅動投資的細節。

為什麼形式化驗證改變了賭注

過去兩年的大多數時間裡，AI 輔助數學的瓶頸並不在於生成候選論證。模型擅長產出看似合理的推理。瓶頸在於判斷其中哪些是正確的，因為檢查一份證明既慢、又依賴專家，還難以並行化。

Lean 把這一點反了過來。一旦某個陳述被形式化，驗證就變得廉價而快速，而且值得信賴，因為它靠的是機械流程而非社會共識。55萬行才是昂貴的部分，而一個團隊加上一百個 agent 能在五天內產出它們，才是這裡真正的進步。它暗示：當生成這一端的瓶頸早已鬆動時，驗證這一端的瓶頸或許也正在放寬。

實驗室表示，會把該工作流打包為其科學發現平台上可重複使用的數學驗證模組，把模型、agent、資料與實驗設備連接起來。它還提到一項更早的成果：Wuhan University（武漢大學）的一支團隊曾用該平台，把某個電化學合成製程的研發週期從五到十年縮短到一到兩年。

可以從中讀出什麼

誠實的總結是：這是一個真實的結果，有真實的證明，而產出它的工作流仍然高度依賴人力。七輪專家引導，並不是一個模型在自行運轉。一篇附有 AI 使用聲明的單作者論文，也不是模型在邀功。

發生變化的是，這個閉環現在合上了。模型能在一個無人解決的問題上產生足夠分量的推理，人能引導它，而證明助手能認證結果，無需任何人去信任一份摘要。這是一條流水線，而不是一次展示；而正是一條條流水線，把一項能力變成一種實踐。

下一個問題是：這是否能推廣到那些根本無法形式化的情形之外。幾何與動力系統具有某些適合機器檢查的結構。而科學的其餘大部分並不如此；恰恰是在生物學、材料與醫學這類更混亂的領域，AI 作為研究助手的承諾才會真正受到檢驗。Ghys 的結果說明這件工具能用。它還沒有說明能有多常用。