機器生成數學證明出現路線反轉

GPT證千禧年難題成果大反轉！OpenAI自己沒看懂就發… henry 2026-10-16 13:00:39 來源：量子位 OpenAI的證明，原來沒走「西班牙路線」？henry 發自 凹非寺 量子位 | 公眾號 QbitAI 虧賊！OpenAI的納維-斯托克斯方程連續劇，居然又又又反轉了。。。一個多月前，OpenAI剛宣佈攻克這道懸賞100萬美元的千禧年難題，就被數學家質疑研究成果的原創性。當時，包括OpenAI自己在內，各方都認為，這份長達166頁的證明沿用了兩名西班牙數學家提出的研究路線。

然而現在，隨著數學家們逐漸啃懂那份長達166頁的證明，事情出現了意想不到的變化： OpenAI最終採用的證明方法，根本不是此前大家以為的那條「西班牙路線」。更離譜的是，就連OpenAI都沒搞懂自家模型研究了個啥……就稀裡糊塗地在發佈時說沿用了「西班牙路線」。這事兒是怎麼發現的？在《科學美國人》最新發表的追蹤報道中，記者採訪了多個正在研究這份證明的專家團隊。這些專家越來越確信，OpenAI最後完成證明時，實際上採用了另一套不同的方法。瑞士洛桑聯邦理工學院（EPFL）數學家Gonzalo Cao-Labora直言： 深入研究具體細節之後，就會發現這是一種不同的方法。

好傢伙，OpenAI自己的模型完成了證明，結果公司自己都沒搞清楚它究竟是怎麼做出來的，就端上來了—— 真就端到端，至於怎麼端的，你別管！也真別怪陶哲軒有意見吧（doge）。OpenAI的證明，原來沒走「西班牙路線」？要理解這次反轉，還得簡單回顧一下，OpenAI究竟解決了一道什麼題。納維-斯托克斯方程，描述的是水、空氣等流體如何運動。但數學家始終沒能證明，一個最初平滑、正常的三維流體，在方程描述下，是否會永遠保持平滑。還是說，它可能在有限時間內突然出現奇點，讓局部流速衝向無窮大？後一種情況，在數學上被稱為「有限時間爆破」（finite-time blowup）。

2000年，克雷數學研究所將其列入七大千禧年難題之一，懸賞100萬美元徵求證明。而OpenAI在今年9月給出的答案就是：真的會爆。不過，它證明的並非沒有外力時，流體自己能否出現奇點，而是通過構造特殊的平滑外力，推動流體在有限時間內發生爆破。這種情況符合克雷數學研究所公佈的C、D兩種命題要求，但數學家更關心的無外力版本，至今仍未解決。而這次爭議中的兩條研究路線，恰好都在利用官方題面允許外力的這一點。先來看所謂的「西班牙路線」。此前，西班牙數學家Diego Córdoba和Luis Martínez-Zoroa提出了一種研究方法：通過精心安排外力，不斷推動流體進入極端狀態，最終讓方程出現奇點。

此後，紐約大學數學家Tristan Buckmaster和Anthropic員工Levent Alpöge接著往下研究，藉助Claude、Codex等AI模型，證明了歐拉方程等相關流體方程可以在平滑外力下發生爆破。而OpenAI公佈的納維-斯托克斯證明，同樣使用了平滑外力。加上雙方研究成果發佈時間接近，甚至一度引發了研究成果歸屬的爭議。因此，此前大家普遍認為：OpenAI沿著西班牙數學家鋪好的道路，完成了最後一步。但現在看來，事情並非如此。《科學美國人》最新報道指出，雖然兩種方法都利用外力實現爆破，但OpenAI最終證明中構造外力的方式，與西班牙路線完全不同。

換句話說，兩邊雖然都利用了同一個題目條件，卻採用了不同的數學方法。不過，事情還有一個細節值得注意。OpenAI最初使用過規模較小的Agent團隊，完成一箇中間證明。一些專家認為，這個早期結果確實可能沿用了西班牙路線。但隨後，規模擴大到約1萬個Agent的系統，似乎發現要完成最終證明，還需要換一條路。因此，最終證明的方法不同，並不意味著此前的研究思路完全沒有發揮作用。至於模型是否通過訓練接觸過其他研究者的數據，OpenAI已經公開否認，但外界仍然無法獨立核查。普林斯頓高等研究院數學家Camillo De Lellis也認為，這場爭議恐怕很難得到明確的事實性結論。

OpenAI也沒有真正理解自己模型給出的證明 比起此前的成果歸屬爭議，《科學美國人》這次報道還揭示了一個更值得關注的現象： AI已經能完成連開發者自己都難以理解的數學證明。9月8日公佈成果時，OpenAI高管曾反覆表示，證明沿用了西班牙數學家的研究路線。直到一個多月後，外部數學家深入研究才發現，兩者實際上採用了不同的方法。《科學美國人》由此給出了一個直接的判斷：OpenAI沒有真正理解自己模型給出的證明。而且，直到現在，數學界也尚未完全理解它。這說起來就很怪了，OpenAI並不是沒有驗證這份證明。除了166頁的論文，系統還生成了對應的Lean形式化代碼，可以逐步檢查數學推導是否成立。

只是問題在於，證明在形式邏輯上成立，與人類真正理解其中的數學思想，顯然是兩回事。Lean能夠幫助檢查推導，卻不會自動告訴數學家，這套方法為什麼有效、與已有研究有什麼聯繫，以及能否推廣到其他問題。所以，即便有了形式化代碼，專家們仍然需要藉助其他大語言模型，重新梳理和理解這份證明。而就在數學家們還沒啃完這道題時，OpenAI又一口氣公開了722篇數學手稿，涵蓋372組研究成果。其中涉及霍奇猜想、準黎曼猜想、BSD猜想等一系列重大數學問題。當然，這些成果的核驗進度各不相同，部分還沒有完成Lean形式化。但數學家們已經開始有點跟不上了。

比如，以陶哲軒為代表的數學家們就曾多次表示，AI生成新證明的速度，遠遠超過了人類理解和消化它們的速度。而納維-斯托克斯這次反轉，恰好把這種矛盾暴露出來。過去，數學家通常是先理解問題、建立方法，再逐步寫出證明。如今，AI可能先把證明交出來，人類再回過頭研究它到底是怎麼做的。因為你不會，所以你才會，這句話是個哲學～ 現在我悟了！原來這句話是在說AI做數學題啊！參考鏈接 [1]https://www.scientificamerican.

com/article/openais-blockbuster-navier-stokes-proof-isnt-what-we-thought-it-was/ 版權所有，未經授權不得以任何形式轉載及使用，違者必究。