OpenAI 下一代模型 Astra 解出 10 道逾十年未解數學難題
OpenAI 以一種不太尋常的方式預告了它的下一代模型家族「Astra」：直接公布它在 10 道長年未解的數學與理論計算機科學難題上做出的成果。據 OpenAI 研究員 Noam Brown 於 8 月 1 日發布，一個內部版本的 Astra 對這 10 個問題給出了解答，而這些問題「至少十年、多數更久都沒有人取得進展」。這是 AI 在科學推理上的一大步，但也有幾個必須先講清楚的但書。
10 道難題橫跨多領域，含 Erdős 老問題與「非索菲群」
這些問題橫跨高維幾何、編碼理論、群論、量子複雜度、格密碼學與極值組合等領域。其中幾個具指標性：一是解決了群論裡「非索菲群（non-sofic groups）是否存在」這個重大的未解問題；二是 Erdős 早在 1946 年提出的「平面單位距離問題」相關進展；理論計算機科學方面，也包含計算矩陣 permanent 的新電路複雜度下界。Astra 被定位為「長時推理」模型，能協調多個智能體，在數小時到數天的尺度上處理複雜問題—這正是攻這類難題所需的持久推理能力。
AI 出論證、人類寫論文、Lean 機器驗證
這裡的分工方式是關鍵。OpenAI 表示，數學論證本身「來自 Astra」，人類研究員則協助把結果整理成論文、並將證明形式化。關鍵在於最後這一步：每個解答都被寫成形式化證明語言 Lean 的證書，也就是「機器可檢驗的正確性憑證」。這一點很重要—它意味著這些證明的邏輯正確性不是靠人相信 AI，而是能由電腦逐步驗證。成本方面，OpenAI 稱以其 Sol 模型的 API 費率換算，這些解答的 token 成本約在 2,000 美元等級，並強調每題花費其實不高，算力還能再往上加。
廣告 - 內文未完請往下捲動
該興奮，但也要有分寸
幾個但書要放在一起看。第一，這是 Astra 的「內部、未發布」版本，不是公開可用的模型，Noam Brown 也明講是 internal version。第二，Lean 能驗證證明的「邏輯正確性」，但一個結果在數學界的「重要性與新穎性」仍要經過同行評審與時間檢驗，這部分尚未完成。第三，Noam Brown 主動點出限制：他們試過其他更大的問題但沒成功，也還沒解出任何「千禧年大獎難題」。即便如此，外部數學家已給出正面評價—Thomas Bloom 稱這是「大新聞」。把這幾點合起來，比較準確的說法是：AI 首次在多個長年未解的真問題上，以可機器驗證的方式做出貢獻，這是研究級推理的一個實質里程碑，而不是「數學被 AI 解完了」。這也延續了近期 AI 開始能做研究級數學與密碼分析的趨勢。
風險提示
加密貨幣投資具有高度風險，其價格可能波動劇烈，您可能損失全部本金。請謹慎評估風險。
