Astra 是什麼：OpenAI 的次世代模型

OpenAI 在 2026 年 7 月 29 日的公告 中宣布，旗下尚未對外發布的次世代模型 Astra，在 10 道長期未解的數學與理論資訊科學難題上取得新結果。公告原文寫道，這些結果「由 Astra 的內部版本、我們的下一個主要模型所達成」。

這不是 OpenAI 第一次用未發布模型挑戰開放問題。公告提到，2026 年 5 月該公司曾分享一個 AI 生成的反證，推翻 Erdős 的單位距離猜想（unit-distance conjecture）。把未發布模型推向開放數學問題，已是大型實驗室展示推理能力的慣用手法——未發布研究版 Claude 先前也曾推進黎曼猜想零點下界，而 Astra 這次的範圍橫跨更廣的學科。

十道難題：從球體堆積到極值組合

依 OpenAI 公告列出的十道難題，結果涵蓋高維幾何、編碼理論、算術電路複雜度、群論、算子代數、量子複雜度、格密碼學與極值組合等領域，整理如下：

  1. 高維球體堆積：對球體堆積密度給出逼近 Cohn–Elkies 閾值的新上界。
  2. 二元碼與球面碼：對任意指定最小距離下的二元碼最大規模，給出指數級改善的界，高維球面碼有相應結果。
  3. 非 sofic 群：以建構證明非 sofic 群存在，回答群論的核心開放問題。
  4. Connes 剛性猜想：反證「某些群由其 von Neumann 代數唯一決定」的長期猜想。
  5. 算術電路複雜度：對以算術電路與公式計算 permanent 給出新下界，含 n⁴/log n 階的算術公式下界。
  6. 量子平行重複：對一般兩玩家量子賽局給出指數級平行重複定理，延伸自古典複雜度理論的基礎原理。
  7. 最近向量問題：對這個與後量子密碼學相關的格問題，給出多項式因子的近似硬度。
  8. Ehrhart 體積猜想：在每個維度決定「重心為唯一內部格點的凸體」之最大可能體積。
  9. 多色 Ramsey 數：對多色三角形 Ramsey 數給出超指數級下界，解決 Erdős 問題 183。
  10. 極值數猜想：處理極值圖論的緊緻性與退化性猜想，解決 Erdős 問題 146 與 180。

OpenAI 的措辭是這些結果「解決或在長期未解問題上取得實質進展」——亦即並非十道都被完整解決，部分是新上界、新下界或反證。

Lean 證明為何是可信度的關鍵

Lean 證明查驗示意
圖1　Lean 把每一步推論寫成可被機器逐步查驗的形式，是這次結果可信度的核心支柱。

OpenAI 表示，Astra 找到解答後，由人類搭配同一模型將論證整理成手稿，再由模型把每個論證形式化為 Lean 證明（Lean certificate），並釋出模型思考過程的紀錄。Lean 是互動式定理證明器，會從公理出發逐步檢查推論是否成立；一個能通過 Lean 編譯的證明，其邏輯正確性可被任何人用機器獨立查驗，不必仰賴作者或同儕審查。另一條從資料與模型切入的路線，可對照 OpenBMB MathForm 的 Lean 自動形式化資料與模型。

不過，機器查驗只保證「形式化後的命題」成立，並不自動保證這份形式化規格精確對應到原本想表達的數學問題。把人類的數學概念翻譯成電腦編碼的過程仍可能出錯——這正是 Leiden 宣言 點出的疑慮：自動化技術產生的論證，困難之一就在於「電腦編碼與人類表述之概念間的翻譯」。

兩千美元的推論成本與歸屬爭議

OpenAI 估算，Astra 找到這些解答所消耗的 token，依 Sol API 費率換算「約合 2,000 美元」。這個數字是「搜尋解答」的推論成本，並不含模型訓練、硬體建置或人力整理手稿的支出，因此不宜直接當成「解一題兩百美元」來解讀。

更值得關注的是歸屬問題。OpenAI 在公告中明確表態：數學論證由模型產生，手稿整理與 Lean 形式化由人類協助完成，正確性由 OpenAI 負責；把「完全由 AI 系統產生的證明」宣稱為人類著作，會同時誤呈系統的貢獻與真正人類智識勞動的性質。這段論述直接回應了數學社群對作者身分與責任歸屬的爭論。

數學社群的雙重反應：興奮與憂慮

數學社群的雙重反應
圖2　面對 AI 進入數學研究，社群同時出現對新發現的期待與對審查、歸屬、自主性的憂慮。

國際數學聯盟背書的 Leiden 宣言 開宗明義描述了這種分歧：研究者的反應「從對其帶來新發現潛力的熱忱、對發展步調的驚懼、對快速變化的漠然，到對其影響的憂慮」都有。宣言由 16 位數學工作者組成的工作小組撰寫，獲 Fields 獎得主 Terence Tao、Peter Scholze 等人連署，主張 AI 對數學研究的核心價值——證明的確定性、作者歸屬、可獨立驗證、研究自主——構成威脅。

Tao 在連署聲明中表示「全心支持這份宣言的陳述與建議」；Scholze 則直言，數學研究的目標是「人類對數學的理解」，因此他思考數學想法時選擇不使用 AI。宣言也警告「透過新聞稿或部落格發布結果、趕在社群審查之前搶市」的做法，並提醒政策制定者「不要相信炒作」，因為科技業有強烈的商業誘因去誇大產品能力。

仍待獨立檢驗之處

這篇報導的第一方依據為 OpenAI 官方公告與 Leiden 宣言。截至目前，Astra 尚未對外發布，外部無法直接複算；十道結果雖附 Lean 證明，仍待數學社群確認每份形式化規格是否精確對應原問題，並評估各結果在學科中的深度與意義。OpenAI 釋出的手稿與 Lean 證明的具體頁數與存放位置，未在本次查證的第一方頁面中明確標示，本篇不作轉述。