OpenAI 8 月 1 日正式將下一代重大模型家族命名為 Astra，並表示其內部版本已在數學與理論電腦科學領域解出 10 個長期無人推進的開放問題。
重點整理：
- OpenAI 在最新報告中確認 Astra 名稱，並歸功該模型於 10 個至少停滯十年以上的難題上取得突破。
- 清單包括建構非 sofic 群、推翻 Connes 剛性猜想，以及解決 3 個源自 Erdős 問題集的難題。
- 所有證明都附有可機器驗證的 Lean 證書，整體推理過程按 Sol API 價格估算，代幣成本約 2,000 美元。
OpenAI Astra 報告列出 10 項數學成果
公司於週六發布長達 249 頁的技術報告，涵蓋球體堆疊、編碼理論、算術電路複雜度、群論、量子複雜度與晶格密碼學等領域。
報告所列問題，在其「核心結果」上至少十年以上沒有實質進展，多數甚至已卡關更久。其中一項建構首次證實「非 sofic 群」確實存在，為群論中的核心懸案畫下句點。
其他成果包括推翻 Connes 剛性猜想、證明 Ehrhart 體積猜想，以及解出 3 個來自 Erdős 問題目錄的難題，其中包含多色三角形 Ramsey 數下界的新結果。OpenAI 估算，Astra 找出這 10 個解答所耗費的代幣成本，約為 Sol API 價格水準的 2,000 美元左右。
Astra 採用多代理架構，將單一高難度任務切分為多個子問題，長時間並行推理後再彙整結論。這個模型家族定位在現有 Sol、Terra、Luna 模型旁邊，這些模型目前掛載 GPT-5.6 標籤。OpenAI 尚未決定是否將 Astra 以 GPT-6、GPT-5.7 變體，或獨立等級的型號推出，也未給出具體上市時程。
延伸閱讀：比特幣 ETF 單日吸金 2.331 億美元 一檔基金包辦大多數買盤
數學家檢視 Astra 的 Lean 形式化證明
曼徹斯特大學數學家、Erdős 問題目錄策展人 Thomas Bloom 在 X 上形容這批結果是「重大消息」，並評價其在「建構」層面的重要性，超過 OpenAI 今年 5 月公布的單位距離反例。
每一項論證都附有可由機器驗證的 Lean 形式化證明，這是多數 AI 研究宣稱難以跨越的門檻。儘管如此，數學界仍須逐一確認這些形式化陳述，是否精準對應到原本被視為「未解」的那個版本的問題。參與推理方法開發的 Noam Brown 則表示，本次成果並未觸及任何千禧年大獎難題。
山姆．奧特曼先在華府閉門簡報推銷 Astra
OpenAI 執行長 Sam Altman 在報告公布前幾天，已於華府與多位參議員及行政部門高層舉行閉門會議，向其展示 Astra 能力。
奧特曼於週三會晤參議員 Raphael Warnock 與 Bernie Moreno，行程中也包括與 Mark Warner、財政部長 Scott Bessent、商務部長 Howard Lutnick 等人的會談。
Astra 預料將成為首批納入聯邦政府「模型事前審查框架」的產品之一。
OpenAI 在今年 5 月已採取類似路線，當時公司以部落格貼文而非期刊論文的形式，宣布 AI 找到 Erdős 單位距離猜想的反例。數學界不久後於 6 月發布「萊頓宣言」，在國際數學聯盟支持下，警示「以新聞稿取代論文評審」的證明模式；OpenAI 在本次技術報告中也特別引用該宣言。