OpenAI 正準備在 GitHub 上一次性發布數百個 AI 生成的數學解答，為該公司在形式數學領域一段極具影響力的工作畫下句點。

這次計劃中的上傳，緊隨 2026 年 8 月 28 日的一項公告，OpenAI 在公告中透露，已開始訓練一個能夠求解 Navier-Stokes 千禧年大獎難題以及其他 100 多個長期未解數學問題的 AI 模型。Navier-Stokes 問題是 Clay 數學研究所指定的七大千禧年大獎難題之一，每個難題的正確解答可獲得 100 萬美元獎金，並位列數學中最深奧的未解問題之中。這些方程本身於 19 世紀提出，用於描述流體的運動；該獎項問題則探討平滑解是否在三維空間中始終存在。

OpenAI 將發布什麼

即將進行的 GitHub 發布預計將包含以 Lean 4 撰寫的形式化證明。Lean 4 是一種證明輔助語言，可讓數學論證由電腦驗證。Lean 4 是開源軟體，並支撐著由社群維護的大型形式化數學函式庫 mathlib；由於以其撰寫的證明經過機器檢驗，一旦結果公開，任何人都可以重新執行驗證。

此前，OpenAI 於 2026 年 8 月創下里程碑，在 GitHub 上發布了 10 個未解數學問題的解答，同樣附有 Lean 4 形式化證明。即將推出的這一批次規模將大得多，被形容為一次重大的集中發布。

OpenAI 發言人 Lindsay McCallum 證實，公司正諮詢其數學與人工智慧顧問委員會，以負責任的方式處理這項披露。截至本文撰寫時，尚未確定具體的發布時間。

數學界存有疑慮

並非數學界的所有人都為此感到振奮。一些數學家對 AI 公司生成並發布證明的速度提出了尖銳的疑慮，批評者更將領先 AI 公司之間的競爭行為做出尖刻的比較。其中一個廣為流傳的說法，將這種動態形容為宛如黑幫行徑——這個詞道出了人們對功勞歸屬、結果驗證速度，以及傳統同儕審查流程能否跟上的焦慮。

數學界現在面臨的更廣泛問題是：當證明由機器產出時，功勞該如何歸屬。如果 AI 解開了 Navier-Stokes 問題，誰能領取千禧年大獎獎金？是訓練模型的團隊？還是將問題形式化的研究人員？這些已不再是假設性的邊緣案例。迄今唯一被解決的千禧年大獎難題是龐加萊猜想，由 Grigori Perelman 證明，而他隨後拒絕了獎金。

為何這次發布值得關注

OpenAI 選擇透過 GitHub 而非傳統學術期刊發布這些結果，本身就具有重要意義。在 GitHub 上發布速度快、公開且具版本控制，但卻繞過了數學界長期賴以驗證的編輯與同儕審查機制。根據 Clay 數學研究所自身的規定，聲稱的解答必須發表於經審查的期刊，並在數學家中維持兩年的普遍認可，才能獲頒獎金。

AI 的解答究竟是完整的、部分的，還是取決於會限縮其適用範圍的假設，正是即將到來的 GitHub 發布需要釐清的細節。OpenAI 與其顧問委員會的互動顯示，公司理解這一點，儘管發布時間表仍未確定。