OpenAI 表示，尚未對外發表的次世代主力模型 Astra 的內部版本，解開了數學與理論計算機科學領域的 10 道未解難題。這些問題都已懸置至少 10 年以上。除了一份 249 頁的手稿，該公司還在 GitHub 上為每項結果公開了可由機器驗證的 Lean 4 證明。這與只是宣稱有所突破的發表方式，在可驗證性上性質截然不同。
不是主張，而是能夠通過編譯的證明
這次發表最值得注意的一點，在於 10 項結果全部附上 Lean 4 證明。Lean 是一套以形式語言撰寫數學證明、再交由電腦進行機械檢查的系統。寫出的證明不是通過就是不通過，過程中的跳躍或含糊其詞都不被接受。
長久以來，AI 產出的證明始終伴隨著一項批評：專家讀懂所需的時間太長，導致獨立驗證難以推進。只要附上 Lean 證明，任何擁有 Lean 編譯器的人都能在自己的電腦上確認結果，不必信任模型本身或營運模型的一方。這可說是針對數學界一再指出的驗證難題，從形式面給出的回應。
懸置 27 年的群論問題獲得解決
10 項成果中被放在核心位置的，是首次給出非索菲群的明確構造。索菲性這個概念由 Mikhail Gromov 於 1999 年提出，是否存在不滿足該性質的群，作為群論的核心問題懸置了 27 年。此前沒有數學家能證明這類群存在，也無法證明其不存在。
其餘 9 項成果橫跨多個領域：推翻了關於馮紐曼代數的 Connes 剛性猜想，證明了 Ehrhart 體積猜想，解決了 Paul Erdos 問題集中的 3 道題（包含涉及多色拉姆西數的第 183 題），自 1978 年以來首度改進高維球堆積密度的一般上界，證明了雙人量子賽局的平行重複定理，並提出計算積和式的電路複雜度新下界。群論、算子代數、高維幾何、量子複雜度、格密碼與極值組合學都在涵蓋範圍內。
10 項成果合計運算成本約 2,000 美元
OpenAI 指出，以 Sol API 的費率換算，解開全部 10 道題的運算成本合計約 2,000 美元（約 31 萬日圓）。該公司數學研究負責人 Sebastien Bubeck 在 X 上確認了這些結果，稱其 beautiful（優美），並說明每項結果都附有 Lean 證明與推理過程的說明。
※1 美元 = 156.5 日圓（截至 2026 年 8 月 3 日）
與數學界的距離依然微妙
不過，這次發表所處的環境並不平靜。6 月，數學家們發表了萊頓宣言，國際數學聯盟也表態支持。宣言警告 AI 企業未經同意使用已公開的研究成果、繞過同儕審查，正在傷害證明與署名的嚴謹性，並點名批評以新聞稿而非同儕審查期刊發布結果的做法。
OpenAI 先前已有前例。5 月，同一長程推理模型系列被指推翻了離散幾何領域懸置 80 年的艾狄胥單位距離猜想。費爾茲獎得主 Tim Gowers 當時表示，他會毫不猶豫地推薦該證明刊登於《數學年刊》。這一次，經營 erdosproblems 網站的 Thomas Bloom 也在 X 上寫道，新成果是重大消息，分量超過單位距離的反例。讚許之聲確實存在，但整個數學界會如何看待透過部落格文章發布的結論，仍沒有答案。
Astra 的真面目尚未揭曉
關於 Astra 本身，OpenAI 沒有提出發表時程，只將其形容為次世代主力模型。包含投資人 Mark Kretschmann 在內的部分觀察者推測它屬於 GPT-6 系列，但並無確切資訊。該公司也在推動面向 10 萬名學術研究者、持續到 2027 年的前沿模型免費使用計畫，與科研領域的連結正持續加深。
總結
一個尚未發表的模型解開了 10 道懸置十年以上的數學難題，而且每項結果都附上可由機器驗證的 Lean 4 證明，這是這次消息的重點。全部運算成本僅約 2,000 美元。提供驗證手段確實是一項進展，但繞過同儕審查發布成果是否恰當的爭議仍未平息，Astra 本身的公開時程也依舊不明。關於數學該如何運用 AI 的討論，接下來應該還會有更多發展。
