簡訊

OpenAI 在 GitHub 上發布了 722 篇數學手稿，分屬 372 個結果家族，全部來自一個尚未公開的內部模型。

OpenAI 发言人表示，這些內容幾乎全部來自一次交給單個 AI 代理的提示詞，不過其中一些可能經歷了多次嘗試。

這是一項大膽的說法，也有可能是數學領域的一項重要突破。但並不是所有人都買賬。

「除非他們公開模型，且人們能夠複現結果，否則我認為任何關於使用單一代理一次性解決問題的說法都應該視為未經證實的，」數學家 Andrew Sutherland 向《科學美國人》表示。「我們應該要求出示證據，」他說。

OpenAI 公布了其中10個結果的簡版推理摘要。同時，根據倉庫中的形式化目錄，這722篇論文中只有162篇帶有經過計算機檢查的主結果，約佔全部內容的22%。這些結果被翻譯成 Lean ——一種會機械檢查每一步邏輯推導的軟件。

OpenAI 也表示，並非所有手稿都有 Lean 的形式化，並稱「部分未形式化的結果可能存在問題」。換言之，他們發布的很多內容可能是錯誤的。

Lean 的檢查通過，只能說明在 Lean 中的陳述是成立的，但這並不能證明該陳述與原始問題完全一致，也不能證明結果是新的或重要的，而這正是數學家現在必須判斷的部分。

而這也是研究人員開始皺眉的所在。

「我試著閱讀 OpenAI 有關平面顏色數大於等於6的證明，但這完全是難以置信的外星數學？模型居然找到了任何K着色與『弱可測』K着色的等價，這似乎憑空出現。」 Dmitry Rybin 在X上寫道。

“openai / math 仓库已经关闭了，Issues，也从未接收过pull request。这非常令人失望。如果你发布了722篇手稿，并要求它们以Lean的形式化，那么就需要一个地方让人们能够提交这些手稿。我目前正在使用Lean来形式化关于Saxl的猜想的证明……”Keith Adler在X上写道。

「現在的狀況是，AI可以在提出問題的人類無法理解、無法驗證、也無法為其負責的情況下輸出數學論證，」普林斯顿高等研究院在一份聲明中表示。「我們認為，人類對數學的理解仍然至關重要。在這個新時代，我們應該如何努力形成一種新的範式，將人類對數學的理解納入負責任的學術成果之中？」

不過，也有一些人持更樂觀的態度。多倫多大學教授 Abhishek Saha 寫道：「今天對數學來說是非常重要的一天。」但他指出，這些問題大多屬於「現有研究計劃中的非凡進展」或「令人驚訝的突破」。

這意味著，這組問題中的大多數都非常有趣，但並不像千禧年難題那樣不可能或具有改變局面的意義。在722個問題中，只有一個屬於那一類：準黎曼假設（Quasi - Riemann Hypothesis）。

「關於 OpenAI 今天發布的372個結果，涵蓋722篇手稿，我還有一些進一步的想法。如果我要按照數學家證明並發表的定理的突破性來分類的話，我會非常粗略地分成四類：A）非突破性……」 Abhishek Saha 在X上寫道。

多倫多大學的數學家 Daniel Litt 則持相反觀點，認為沒有理由要求公司對這些數學問題的答案保密。

Anthropic 上個月對其經過 Lean 檢查的費馬大定理證明採用了不同的方法，將全部1300萬行公開發布到 GitHub 上。那份證明形式化的是 Andrew Wiles 在1995年發表的定理，而不是聲稱提出新的結果。

OpenAI 表示，隨著獲得更多 Lean 的形式化版本，公司會繼續補充；目前，這722篇手稿中已有162篇帶有 Lean 的形式化。