OpenAI 公開 Navier–Stokes 奇異性證明與 Lean 憑證，但數學界驗證才剛開始

OpenAI 9 月 8 日公開一項由內部模型產生的 Navier–Stokes 證明，主張完成克雷數學研究所問題敘述中的反例路線 C 與 D。其構造從平滑、有限能量的三維不可壓縮流出發，施加保持平滑的外力，讓渦旋核心持續向內收縮並沿軸向伸長；速度及方程中的若干項雖趨於無界，對流、壓力、黏滯等成分卻經精細抵消，使外力本身不必奇異。若論證成立，結果表示至少某些合法資料無法維持全域光滑解，而不是提供一般流體模擬的封閉解法。

技術新聞的另一重點是交付形式。GitHub 儲存庫包含分別處理全空間與週期環面的 Lean 證明，鎖定 Lean 4.34.0-rc2、Mathlib 與 Lake；第三方可以下載相依快取後執行 `lake build`，另有 Comparator 挑戰供獨立檢查。這比只發布自然語言論文更容易發現缺失引理、偷偷加入的公理或型別不一致，但 Lean 核心只能確認程式確實推出所形式化的定理，不能自行判定形式敘述是否完整對應原始千禧年問題，也不能替代對數學構造與引用來源的審查。

OpenAI 表示，系統由大量協調代理使用快取網路資料與程式工具，在聽聞相關研究傳言後集中搜尋；所用基礎模型仍未公開，訓練資料、代理軌跡、搜尋成本及失敗嘗試也不足以重現。因此目前應把它視為附可執行憑證的重大候選證明，而非已確認結案。克雷研究所規則要求成果先在合格出版管道發表、至少經過兩年，並獲全球數學界普遍接受，才會進入正式考慮。接下來最值得觀察的是獨立 Lean 重建、分析學家逐步核對形式化與論文的對應，以及公開審查能否找到被形式敘述排除在外的隱含假設。