2026年9月11日，25位菲爾茲獎得主聯名發表聲明，警告人工智慧正在改變數學研究的目標和節奏。聯署名單此後繼續增加，截至9月26日，聲明官網已列出27人，包括陶哲軒、馬丁·海爾和瑪麗娜·維亞佐夫斯卡。

聲明批評AI公司把著名數學難題變成衡量模型能力的排行榜。解決問題原本是獲得概念理解和洞察的手段；如果機器開始批次生產“真或假”的結論，數學可能擁有越來越多答案，卻失去培育思想、訓練學生和傳遞知識的過程。

導火索發生在聲明發表的三天前。

9月8日，ChatGPT開發者、美國人工智慧公司OpenAI宣佈，其內部模型找到納維–斯托克斯千禧年難題的一項解答。納維–斯托克斯方程是描述水、空氣等黏性流體運動的基本方程。困擾數學界近一個世紀的問題是：一個初始狀態光滑的三維流體，會不會在有限時間內突然出現速度趨於無窮的奇點？

OpenAI給出的答案是：會——至少在施加某種光滑外力的情況下會。

公司同時公開了一篇166頁論文和一套Lean形式化證明。Lean是一種開放原始碼的互動式定理證明器，能夠按照形式邏輯規則逐步檢查推導。OpenAI還披露，參與這項工作的AI智能體約有一萬個。

9月11日，負責設立千禧年大獎的克雷數學研究所表示，這個問題“看來已經得到解決”。但芝加哥大學數學家路易斯·西爾維斯特隨後給出了一句耐人尋味的評價：

“克雷問題解決了，但納維–斯托克斯方程最主要的問題沒有解決。”

一句話，把這場爭論劈成了兩半。

數學難題的價值，從來不只是等待一個“成立”或“不成立”。

安德魯·懷爾斯在1994年完成費馬大定理的修訂證明，相關論文於1995年發表。那項工作的份量，並不主要來自確認某個整數方程無解，而在於它把橢圓曲線、模形式和谷山–志村猜想連在了一起。費馬大定理是終點，也是更大理論圖景露出水面的一刻。

電腦輔助證明也早已進入數學史。1976年，肯尼斯·阿佩爾和沃爾夫岡·哈肯依靠電腦檢查大量構型，完成四色定理證明。2005年，喬治·貢蒂埃又用Coq證明助手完成形式化驗證。

四色定理當然已經解決。爭議並未就此消失：如果一項證明只能依靠機器核驗，人類是否算得上理解了它？

這個問題沒有標準答案。數學證明本來就有幾副面孔。它可以確認結論，可以解釋原因，也可以創造新工具。最好的證明往往三者兼具；有些證明只完成第一項。

證明像一張合格證，也像一幅地圖。合格證確認目的地已經到達，地圖則告訴後來者道路為什麼可行，以及它還能通向那裡。

AI帶來的變化，是找到合格證的速度可能遠遠超過繪製地圖的速度。

02 這不是一個沒有推理的黑箱答案

把OpenAI的成果描述成“機器直接吐出答案”，並不精準。

公開論文包含物理圖景、證明綱要和詳細推導，Lean程式碼也已發佈。論文構造了一個不斷收縮、旋轉和拉長的渦旋，再用一系列振盪脈衝產生動量通量，抵消原本會發散的殘餘項。速度最終趨於無窮，能量卻保持有限，施加在流體上的外力仍然光滑。

這是一份分析性證明，不是把無數情況逐一檢查之後得到的統計結論。

“暴力”主要發生在尋找證明的階段。OpenAI稱，相關智能體交換了約270萬條消息，產生約1300億輸出token。系統可以平行嘗試大量構造、淘汰失敗路線，再把有效部分拼接和整理出來。

人類數學家也會經歷相似過程：試錯、推翻、重來、從其他論文借用工具。區別在於，機器把這種搜尋擴大了幾個數量級。

這裡涉及兩種不同的知識生成方式。

數學家面對複雜問題時，常常先憑藉類比、對稱性、幾何想像、量綱分析或思想實驗，判斷哪條路值得走，再把直覺寫成嚴格證明。微積分、廣義相對論和現代數學物理中的許多突破，都不是從一串完整推導開始的。研究者往往先看到某種結構，甚至先有一個難以精準表達的物理圖景，然後才尋找適合它的定義和語言。

AI系統更擅長另一種路徑。它從大量已有文獻和訓練資料中學習模式，再在廣闊的候選空間中高速生成、比較和剪枝。多智能體系統還能把不同路線同時展開，保留局部有效的結果，最後拼接成一條可行證明。

這並不意味著人類擁有神秘靈感，機器只能盲目窮舉。人類直覺本身，也可能是多年訓練和失敗經驗壓縮後的模式識別；AI搜尋同樣會受到既有數學知識和啟髮式策略的引導。

兩者更重要的差別，在於發現過程是否容易被說清楚。

一位數學家通常需要向同行說明，為什麼選擇這個定義，為什麼相信某種結構存在，哪一次失敗改變了研究方向。機器則可能在數百萬條消息中找到一條成功路線，卻沒有把“為什麼應該這樣想”壓縮成可以傳授的判斷。

搜尋規模很大，並不能證明最終方法沒有思想。假如一百萬次嘗試找到一個簡潔、通用的新原理，那依然是數學進步。反過來，一份完全由人類寫成的證明，也可能冗長、特殊，除了當前問題那裡都用不上。

數學可能失去的，不是某種只屬於人類的神秘直覺，而是直覺形成和方法選擇的可見過程。這個過程既產生證明，也訓練下一代研究者判斷什麼值得嘗試。

所以，算力多少並不是判斷數學價值的尺子。更有意義的問題是：這套證明能否被壓縮？其中的構造能否推廣？它有沒有打開新的研究方向？

OpenAI證明對應哪一版納維–斯托克斯問題，是本案最容易被新聞標題抹平的細節。

查爾斯·費弗曼2000年為克雷數學研究所撰寫的官方題目包含A、B、C、D四條路徑。A、B討論無外力情形，C、D允許使用光滑外力。證明其中任何一條，都可以構成對官方千禧年問題的解決。

OpenAI走的是C、D路線：從靜止流體出發，精心設計一個光滑外力，讓流體在有限時間內形成奇點。

從規則上看，這沒有問題。克雷數學研究所的表態也說明，它認真看待這項結果。該所同時提醒外界，候選解答仍需在合格刊物發表，等待至少兩年，並獲得國際數學界的普遍接受，才能進入正式評獎程序。

分歧在於，多數流體方程研究者長期追問的是無外力問題。他們想知道，當沒有人為設計的力量從外部推動時，流體自身的非線性運動能否製造奇點。

西爾維斯特所說的“克雷問題解決了，主要問題沒有解決”，指的正是這道裂縫。OpenAI完成了官方題目允許的一條路線，卻沒有終結學界對無外力流體的追問。

9月17日，彼得·康斯坦丁、米哈埃拉·伊格納托娃和弗拉德·維科爾在預印本平台arXiv發佈論文。該文尚未經過同行評議，也明確表示沒有核驗OpenAI整篇證明。

三人研究了帶有OpenAI構造若干關鍵特徵的解，並證明：如果外力在空間上是實解析的——外力為零自然包括在內——這類解在擬議奇點處仍然保持正則。

這個結果沒有否定OpenAI的受迫爆破解，卻堵住了一條看似順理成章的延伸路線。那套依賴軸對稱核心和特定尺度估計的構造，無法原樣搬到無外力問題上。要繼續往前走，還得出現新的數學想法。

Lean在這裡能做的，是檢查形式化命題是否從給定定義和公理中成立。它不會判斷外力版本是否自然，也不會衡量一個結果距離流體力學家心中的“主要問題”還有多遠。

形式證明像一份逐筆核對無誤的賬單，卻不說明這家公司為什麼賺錢。

這次突破也不是從空白處突然出現的。

從2023年起，迭戈·科爾多瓦和路易斯·馬丁內斯-索羅亞一直在研究如何利用多尺度渦量級聯製造受迫爆破解。簡單說，就是讓不同尺度的渦旋結構逐層放大，再由外力維持整個級聯。

紐約大學庫朗數學科學研究所教授特裡斯坦·巴克馬斯特後來表示，他與Anthropic研究員萊文特·阿爾珀格以這一路線為起點，借助多種AI工具，把相關方案推進到具有光滑外力的歐拉方程。

兩人使用的工具包括Anthropic開發的Claude和OpenAI提供的Codex。Anthropic是OpenAI在前沿模型領域的直接競爭對手。阿爾珀格的身份，也讓隨後發生的優先權爭議多了一層公司競爭色彩。

按照巴克馬斯特公開的時間線，兩人在8月15日取得受迫歐拉方程結果，8月22日完成Lean驗證。9月3日，科技圈開始流傳“Anthropic解決了一個重大數學難題”的消息，他隨即主動聯絡OpenAI。9月6日，OpenAI告訴他，公司內部模型已經得到了受迫納維–斯托克斯證明。

巴克馬斯特與阿爾珀格此前一直使用Codex處理研究工作，並把項目草稿輸入相關會話。這使他擔心，OpenAI的模型或研究團隊是否可能從未發表材料中獲得線索。

他沒有指控OpenAI竊取成果。在9月7日晚公開的聲明中，他寫得很謹慎：“我不知道我們的資料是否被使用。”

OpenAI最初表示，雖然可能性很低，但不能完全排除由產品使用行為產生的去標識化資料曾幫助改進模型。9月10日，公司更新公告稱，經過調查，巴克馬斯特此前兩個月的Codex提示不可能以任何方式影響此次使用的內部系統，包括通過訓練；OpenAI還表示，研究團隊和智能體在相關工作公開前沒有接觸兩人的具體成果。

公開資訊不足以證明發生了不當使用。問題仍然存在：一位研究者把未發表草稿交給商業模型時，模型提供者能否同時成為他的競爭者？

這已經超出普通的隱私政策。科研人員需要知道，草稿是否進入訓練，內部團隊能看到什麼，模型改進資料如何與前沿研究隔離，出現相似成果時又由誰審計。

署名同樣難辦。科爾多瓦和馬丁內斯-索羅亞開闢了外力級聯路線；巴克馬斯特和阿爾珀格借助AI把它推進到新方程；OpenAI再呼叫一萬個智能體完成更遠一步。傳統論文習慣於尋找一組明確作者，卻很難容納這樣一條由公開論文、私人草稿、多個模型和公司算力共同組成的發現鏈。

OpenAI稱，智能體從啟動到得出納維–斯托克斯解答用了約88小時；此後的Lean形式化和驗證又用了17小時。

這個數字最值得注意的地方，不是機器又一次比人快。它改變了科學競爭的時間單位。

過去，研究者得到一個重要想法後，會花幾個月甚至幾年檢查細節、整理證明、與同行交流，再寫成論文。這樣的慢節奏既有低效的一面，也給學術共同體留下了確認來源、修正錯誤和理解方法的時間。

當機器可以在幾天內完成大量技術工作，這些環節就會受到擠壓。等待論文寫得更清楚，可能意味著別人已經借助AI越過你；公開一個尚未完成的方向，又可能等於把路線交給擁有更強模型和更多算力的競爭者。

巴克馬斯特在聲明中承認，他們公開的論文遠未達到理想的寫作標準。他特別形容歐拉方程那份稿子是“AI垃圾”（AI slop）。之所以匆忙發佈，正是因為OpenAI的結果即將公佈。

這可能是AI進入數學之後最先顯現的副作用：論文生產加快，學術交流卻變得更加防備。

另一場更直接的危機發生在同行評議環節。

機器用約88小時生成一篇166頁論文和大規模Lean程式碼，少數具備相應專業能力的數學家，卻可能需要幾個月甚至幾年，才能檢查命題範圍、核對關鍵估計、復現形式化環境，再判斷其中是否包含值得推廣的新思想。

形式驗證緩解了一部分壓力，卻沒有消除審稿工作。Lean可以檢查程式碼內部是否成立，無法自動確認形式化命題與自然語言聲明完全一致，也不能判斷先行工作是否引用充分、方法是否新穎、結論是否被媒體誇大。

這形成了一種新的算力不對稱。證明生產端擁有成千上萬個智能體，驗證端仍然依賴少數專家的大腦和時間。生產一篇論文的邊際成本迅速下降，審查一篇論文的成本卻沒有同步下降。

如果AI實驗室可以批次生成複雜成果，而學術共同體只能逐篇人工消化，同行評議就可能從質量控制機制變成整個知識生產體系的瓶頸。最先耗盡的不是待解問題，而是專家的注意力。

菲爾茲獎得主的聯署聲明針對的也是這一點。他們沒有說機器證明天然低劣，也沒有否定OpenAI結果的數學價值。他們反對的是把著名難題變成模型競賽項目——誰先解出一道名題，誰就在能力排行榜上得分，至於證明是否寫清楚、前人工作是否得到精準引用、方法能否進入數學教材，都可以稍後處理。

可數學恰恰依賴這些“稍後處理”的工作。

一份證明從發表到進入數學知識體系，通常還要經過報告、討論、簡化、重寫和教學。有時需要幾年，有時需要一代人。機器能夠縮短找到證明的時間，卻沒有自動完成這條傳遞鏈。

如果未來每天都有大量形式正確的新結果出現，數學將從“證明稀缺”走向“理解稀缺”。難題不再缺答案，缺的是能夠審查答案的人、判斷意義的人，以及把數百頁技術論證整理成幾個核心概念的人。

傳統期刊制度默認了一種稀缺關係：產生重要證明很難，能夠審查它的同行雖然不多，但論文數量總體可控。AI正在打破這個前提。

制度改革的第一步，是把“證明正確”和“已經理解”分開。

一項AI成果可以先獲得“形式驗證通過”的狀態，再分別接受命題對應性、獨立復現、概念解釋和方法推廣等審查。期刊不必扣押一個可能正確的結果，也不應讓一次Lean通過被誤解成所有學術問題都已解決。

第二步，是設定“可評議性門檻”。

AI生成的重大成果不能只提交一篇超長論文和一套程式碼，把全部消化成本轉嫁給審稿人。提交者還應提供簡明的證明架構、關鍵引理之間的依賴關係、自然語言命題與形式化命題的對應表、相比先行工作的新增部分、已知限制，以及可以獨立運行的驗證環境。

如果作者無法把機器產出的證明整理到可評議的程度，期刊可以暫緩送審。誰生產結果，誰就有責任降低審查成本。

第三步，是把核驗從無償勞動變成正式研究工作。

一篇工業級AI論文可能需要領域數學家、形式化專家、軟體工程師和數學史研究者共同審查。這樣的工作不應繼續由兩三位匿名審稿人在業餘時間完成。基金會、學會和期刊可以設立獨立驗證基金，為復現、審查和證明壓縮提供經費。

驗證者的貢獻也應公開記錄。發現漏洞、確認形式化對應、重寫關鍵證明，都應該成為可以引用的學術成果，而不是藏在匿名審稿意見裡。

第四步，是重寫貢獻和署名規則。

未來的論文需要分別說明：誰提出研究路線，誰發現關鍵構造，誰完成證明搜尋，誰負責形式化，誰獨立驗證，誰壓縮和解釋了證明，模型和算力又由誰提供。AI可以不成為作者，因為它無法承擔責任，但它在研究中的具體作用不能被壓縮成一句籠統的“使用了AI”。

第五步，是讓“地圖繪製”獲得獨立地位。

將百頁機器證明壓縮成短證明，找出決定性機制，把一次性構造推廣成一般理論，證明某條機器路線無法繼續，或者寫出可以進入教材的版本，都應擁有正式論文類型、獨立引用和明確的晉陞價值。

知識壓縮不是科普附屬品。它本身就是研究。

研究機構評價數學家時，也不能只看誰最先解決問題。一個方法被多少後續工作採用、一篇解釋性論文降低了多少學習成本、一套形式化資源是否成為公共基礎設施，都應該進入招聘、基金和獎勵體系。

第六步，是給尚未完成的思想提供安全的優先權記錄。

數學學會或期刊可以建立帶時間戳的保密登記庫。研究者不必公開全部草稿，只需登記核心猜想、證明路線、關鍵構造、合作者以及使用過的AI工具。材料在約定期限內保持封存，只在發生優先權爭議時由獨立委員會調閱。

這可以減少研究者為了自保而匆忙發表不成熟論文，也能讓尚未完成的思想留下可核查的來源。

提供科研AI的平台則應建立更嚴格的資料防火牆。使用者研究資料默認不進入訓練和模型改進，產品團隊與內部研究團隊實行權限隔離，敏感資料訪問留下不可修改的日誌，並接受第三方審計。平台一旦參與相同課題，也應主動披露潛在利益衝突。

彙整鉅亨號中所有使用「AI證明」關鍵字，所發布的內容 (依照時間排序，最新在前，舊的在後)`

一萬個AI、88小時與一道千禧難題：數學正在失去什麼？