OpenAI 8 月 1 日正式將其下一代重大模型系列命名為 Astra，並表示一個內部版本已在數學及理論計算機科學領域上，解出十個長年無人推進的開放難題。
重點摘要：
- OpenAI 在最新技術報告中確認 Astra 名稱，指該模型為十個至少十年無實質進展的難題給出新結果。
- 清單涵蓋非 sofic 群的構造、Connes 剛性猜想的否證，以及三個源自 Erdős 問題庫的難題。
- 每個論證均附上可由 Lean 自動核查的形式化證明，推理全程估計僅花約 2,000 美元（按 Sol API 收費計）。
Astra 報告列出 10 項數學突破
OpenAI 於週六發表長達 249 頁的技術報告，內容涵蓋球體堆積、編碼理論、算術電路複雜度、群論、量子複雜度及格子密碼學等多個前沿領域。
報告中的每個問題，至少已有十年在核心結果上毫無進展，部分甚至停滯更久。其中一項關鍵構造證明「非 sofic 群」確實存在，為群論中一個核心懸案畫上句號。
其他成果包括推翻 Connes 的剛性猜想、證明 Ehrhart 體積猜想，以及解決 Erdős 問題庫中三個著名難題，其中包括多色三角形 Ramsey 數下界的問題。
OpenAI 稱，系統為這十項結果進行搜尋與推理的累計算力開支，按 Sol API 當前價格估算約為 2,000 美元。
Astra 採用多智能體架構，將單一高難度任務拆分為多個子任務，長時間並行運算，再整合各路推理結果。該系列與掛上 GPT‑5.6 標籤的 Sol、Terra、Luna 模型並列。
OpenAI 暫未決定 Astra 將以 GPT‑6、GPT‑5.7 變體，抑或獨立產品線形式推出，亦未公布具體上市時間表。
延伸閱讀：比特幣 ETF 淨流入 2.331 億美元 單一基金幾乎包辦
數學界審視 Astra 的 Lean 形式化證明
曼徹斯特大學數學家、Erdős 問題庫整理人 Thomas Bloom 在 X 上形容相關結果是「大新聞」，並評價這批成果，在「構造」層面上，甚至超越 OpenAI 今年 5 月公開的單位距離反例。
是次每項論證都附上可機器檢驗的 Lean 證書，這一門檻以往極少有 AI 研究成果能達到。不過，數學界仍需逐一核對形式化陳述，是否精確對應原本被視為「未解」的問題。
參與系統推理方法開發的 Noam Brown 則在文章中強調，是次沒有觸及任何「千禧年難題」。
Sam Altman 華府閉門展示 Astra
OpenAI 行政總裁 Sam Altman 在技術報告發布前數日，已於華盛頓向參議員及政府高層閉門示範 Astra 的能力。
Altman 於週三會見參議員 Raphael Warnock 及 Bernie Moreno，行程亦包括與 Mark Warner、財長 Scott Bessent 及商務部長 Howard Lutnick 的會談。
市場預期，Astra 將成為首批按聯邦政府計劃中的「模型預先審查框架」提交審核的大型模型之一。
OpenAI 其實早在 5 月已採取類似路線——當時公司透過官方博客，而非學術期刊，公布利用 AI 推翻 Erdős 單位距離猜想的結果。
其後 6 月，數學界以「萊頓宣言」回應，由國際數學聯盟背書，警告對「新聞稿式證明」應保持審慎。OpenAI 在最新報告中亦主動引用該宣言。
