在一場世界科學節 10 月 2 日的訪談中，數學家 Tristan Buckmaster 描述了一項由 AI 產生的成果；他認為成果正確，但其他數學家很難讀懂。他的說法為近期 Navier–Stokes 公告提出一個更具體的問題：當可讀的說明還需要進一步整理時，研究社群要如何檢視形式化論證？

Buckmaster 討論的是他與 Levent Alpöge 合作研究具有平滑外力的三維 Euler 方程。他們的成果不同於OpenAI 9 月 8 日的主張所涉及的具有平滑外力的 Navier–Stokes 方程。Navier–Stokes 方程包含黏性，Euler 方程則沒有。OpenAI 發布了一篇論文和 Lean 形式化證明，支持其有限時間內發生破裂的主張。負責管理千禧年獎的機構尚未宣布頒獎。

重大變化

  • 改變了什麼：Buckmaster 首次以親身經歷說明如何使用 AI 生成的論證與 Lean 建立另一項受迫 Euler 方程成果，以及向數學家解釋這類證明仍需投入的工作。
  • 為何重要：形式化檢查可以確認，編碼後的論證是否依據指定定義與依賴關係推導而來。數學家也需要理解定理的含義、其中的思路如何運作，以及它承接了哪些先前研究。
  • 接下來觀察什麼：Clay 對 OpenAI Navier–Stokes 主張的評估、可讀的證明說明，以及對作者身分與研究成果取得方式的公開討論，將顯示這項成果如何受到評價。Buckmaster 對成果的信心是專家看法，不代表獎項決定。

經過檢查的論證仍需要解說

在訪談中，Buckmaster 表示，他最初以 AI 產生的 Euler 證明混合了有用想法、無關計算與難以閱讀的文字。他的團隊先讓其他代理檢查個別步驟，再將論證轉成 Lean 進行形式化檢查。他說，儘管表達方式很差，最後的證明仍然正確。這段說法指的是他的 Euler 研究；不應將其視為他獨立驗證了 OpenAI 另一篇 Navier–Stokes 論文的所有部分。

這項區別有實際意義。Lean 會在指定的證明環境中檢查經精確形式化的命題，但它本身不會讓長篇論證變得易讀，也不會讓研究者更容易重用其方法。Buckmaster 告訴 Brian Greene，其他 AI 系統能解析他覺得幾乎無法閱讀的段落，而請 AI 將其轉成一般數學語言也成為工作的一部分。他也說，即使已發表的 PDF 難以閱讀，他仍能理解 Navier–Stokes 論證中的想法。這些是他陳述的看法，不是 BIG CHANGE 對證明的審核；我們沒有執行 Lean 檔案，也沒有評審任一個定理。

NYU Courant 的9 月 14 日說明將 Buckmaster 與 Alpöge 的成果描述為：在平滑外力與有限能量初始資料下，受迫三維 Euler 方程在有限時間內失去正則性。說明指出，合作團隊的三篇論文以 Lean 形式化，並將成果放在 Diego Córdoba 與 Luis Martínez-Zoroa 開始的研究路線中。這些細節對成果歸屬很重要：模型生成的證明可以延伸既有數學路線，但不應抹去建立該路線的人。

同一快速發展過程中的兩項結果

OpenAI 表示，其內部代理系統最先產生了一項無外力 Euler 結果，隨後將這條研究路線用於另一項 Navier–Stokes 建構。其公告承認 Buckmaster 與 Alpöge 的受迫 Euler成果具有優先性，同時表示 OpenAI 的證明是獨立完成的。Buckmaster 在訪談中指出，兩者的數學機制彼此相關，並表示 OpenAI 加入了塌縮渦旋的想法來處理黏性。各方說法都指出兩項主張涉及不同方程與不同證明步驟，但無法解決所有關於時間先後或學術貢獻歸屬的問題。

另外，歐洲數學學會對這項公告表示歡迎，同時強調較早的研究成果，並呼籲關注作者身分、貢獻歸屬與取得內部模型的方式。Clay 於 9 月 11 日的回應指出 Navier–Stokes 問題似乎已經解決，並表示評估成果與確認貢獻歸屬會刻意採取較慢的步調。Buckmaster 告訴 Greene，他相信 OpenAI 已找到解法。讀者可以同時看待這兩種說法：專家的正面評估，以及機構仍在進行的評估。

近期的OpenAI 撤回另外三篇數學論文 是另一件獨立事件。他們報告的符號錯誤，說明應逐一檢視各項主張；但這並非 Navier–Stokes 證明也有同樣錯誤的證據。BIG CHANGE 的論文庫檢視指南說明如何尋找論文版本與證明材料，而我們的審查能力觀點主張應為解說與檢查提供專門支援。較早的 Navier–Stokes 報導記錄了這一連串事件的起點。這次訪談補上了執業數學家對 AI 系統產生論證後續工作的說法。

對如此重大的主張，接下來有用的公開材料應包括精確且易讀的說明、可供檢視的形式化成果，以及獨立的數學界回應。每一項都有不同作用。快速產生候選證明，讓這些工作更加迫切；Clay 所述的程序則保留了仔細處理的空間。

來源與延伸閱讀