OpenAI 在官方部落格宣布，下一代主力模型「Astra」內部版本首度曝光，解開十道停滯十年以上的數學與理論電腦科學公開難題，總成本約 2,000 美元，論證經 Lean 形式化並開源驗證。
（前情提要：OpenAI 推理模型破解 80 年數學謎題，三位頂尖數學家背書）
（背景補充：OpenAI 免費開放 GPT-5.6 Sol，助 10 萬科學家加速研究）
數學界習慣用「年」丈量進度，一篇證明從投稿到同行評審拍板，動輒得熬過兩三年。但 Openai 下一代模型「Astra」，在同一個運算批次裡，把好幾道長年卡關的公開問題接連處理完。
怎麼證明模型沒說謊？
光靠模型宣稱解出難題，數學界不會照單全收。OpenAI 在官方部落格公布的驗證機制分兩層：第一層，人類研究者與同一模型合作，把論證整理成一份 249 頁手稿；第二層，模型把每條論證重新形式化，寫成 Lean 證明，電腦可逐行驗算、不接受跳步的機器可驗證憑證。
整份 Lean 證明庫已開源在 GitHub 上，任何人可下載驗算，每一題還附上模型自述的思考過程。
十道難題，長什麼樣？
操刀者是 OpenAI 下一代主力模型「Astra」的內部版本，這也是 Astra 這個代號首度公開。十項成果全指向停滯十年以上的公開問題，涵蓋純數學到理論電腦科學：
- 高維球體堆積：上界逼近 Cohn，Elkies 門檻
- 二元碼與球面碼：上界指數級改進
- 非 sofic 群：構造出非 sofic 群，回答群論核心公開問題
- Connes 剛性猜想：證偽，部分群不再被馮諾伊曼代數唯一決定
- 算術電路複雜度：給出 permanent 新下界
- 量子平行重複：證出雙人量子賽局的指數平行重複定理
- 最近向量問題（CVP）：證明多項式因子近似難度，牽動後量子密碼學
- Ehrhart 體積猜想：確定每個維度的最大體積
- 多色 Ramsey 數：超指數下界，解決 Erdős 第 183 題
- 極值圖論：一次拿下 Erdős 第 146、180 題
OpenAI 表示，依 Sol API 費率計算，解開全部十題的 token 總成本約 2,000 美元。
今年 5 月，OpenAI 曾公布模型證偽 Erdős 單位距離猜想，催生至少 5 篇後續 arXiv 論文。近期 OpenAI 也推出「ChatGPT for Academic Researchers」，讓 10 萬名科學家免費用最強模型。
數學界為什麼皺眉？
菲爾茲獎得主 Timothy Gowers 稱這是「AI 輔助數學的里程碑」，Erdős 問題目錄維護者 Thomas Bloom 表示，就構造性成果而言是大新聞。
但讚賞背後，今年 6 月，國際數學家群體發布萊頓 AI 與數學宣言，獲國際數學聯盟背書，24 小時內逾 1,000 人簽署，包括 Kevin Buzzard、Peter Scholze。宣言反對三件事：未經同意拿論文當訓練資料、繞過同行評審直發媒體、不註明成果承襲誰的工作。
OpenAI 這次選擇部落格直發而非投期刊，恰好踩在宣言批評的模式上。對此 OpenAI 回應：「AI 能參與數學研究所引發的問題，不是一家科技公司能獨自回答的」，OpenAI 為正確性負責，但論證本身是模型生成。這句話聽起來謙遜，實際上也是宣示：證明的署名權，以後未必理所當然屬於人類。
當解題速度快過同行評審的節奏，真正被考驗的不是模型，而是整套學術信任機制還跟不跟得上。
📍相關報導📍
數學界 Jacobian 猜想遭證偽，OpenAI 研究員：Codex「無網路輔助」也算出來了
