OpenAI 公佈未發布嘅 Astra 模型破解十條懸而未決嘅數學問題，成本只需約 $2,000，全部用 Lean 4 驗證，但學界反應兩極

Astra 到底解咗啲咩問題？

呢 10 條結果橫跨嘅領域好闊，包括高維幾何、編碼理論、算術電路複雜性、群論、算子代數、量子複雜性、格密碼學同極值組合數學 。

1. 高維球體堆砌——將球體堆砌密度嘅上界推到 Cohn–Elkies 界限 。
2. 二進制同球面碼——對任何指定最小距離嘅最大碼大小，畀出指數級嘅改進界限 。
3. 非 sofic 群——首次顯式構建出非 sofic 群，解決咗群論入面一個核心嘅開放問題 。
4. Connes 剛性猜想——推翻咗一個關於 von Neumann 代數嘅長年猜想 。
5. 算術電路複雜性——對計算 permanent 函數畀出更低嘅界限，包括一個 n⁴/log n 級別嘅公式下限 。
6. 量子平行重複——對一般兩玩家量子遊戲證明咗一個指數級嘅平行重複定理 。
7. 最接近向量問題——證明咗多項式因子嘅近似困難性，係後量子密碼學嘅基礎 。
8. Ehrhart 體積猜想——確定凸體嘅最大可能體積，呢個凸體嘅質心係唯一嘅內部晶格點 。
9. 多色 Ramsey 數——畀出一個超指數級嘅下限，解決咗 Erdős 問題 183 。
10. 極值數猜想——證明咗緊緻性同退化性嘅相關猜想，解決咗 Erdős 問題 146 同 180 。

驗證方法：Lean 或者唔算數

OpenAI 冇直接放出 Astra 模型俾人試。佢哋放出嚟嘅係 Lean 4 證明認證，放咗喺 GitHub 上面，用 Apache 2.0 授權，而且報告話「sorry」計數係零——即係成 10 個形式化證明嘅每一步，都係經過完完全全嘅機器驗證 。呢個做法避開咗平時 AI 生成推理到底啱唔啱嘅爭論：證明助理會機械式咁強制執行正確性，唔理個論證係點被發現嘅。

學界反應：有讚有彈，好壞參半

雖然有研究者好似 Noam Brown 咁話呢個公告係科學推理嘅「重大一步」，但同時都有唔少人提出質疑。

唔係最大嗰啲問題。 好多人留意到，呢 10 條問題冇一條係 Clay Millennium Prize 問題（例如 P vs NP、黎曼猜想） 。雖然呢啲問題都係認真好嘢——好似非 sofic 群嘅構建，自 Mikhail Gromov 喺 1999 年引入 soficity 概念以嚟就一直冇人解到 ——但佢哋嘅知名度同影響力始終爭啲。

冇經過同行評審。 呢啲結果係由 OpenAI 直接公佈，冇事先喺數學期刊或者會議上面發表 。批評者話，AI 生成嘅發現同人類協助整理之間嘅界線好模糊，而 OpenAI 自己都引用咗《Leiden Declaration on AI and Mathematics》去承認呢種 tension 。

對一般化能力有保留。 認知科學家 Gary Marcus 就話，喺形式化數學上成功「只係一個特殊情況」，未必能擴展到更廣泛嘅科學推理，而且「喺一個領域嘅專長唔代表喺所有領域都專」。數學本身就容易產生平價、可驗證嘅合成數據，但大部分科學領域都做唔到。

複現性問題。 因為模型冇公開、具體嘅 prompting 方法又冇完全披露，所以外界冇辦法獨立驗證成個生成過程 。有啲批評者就話，冇得接觸 Astra 本身，根本做唔到複現。

商業時機。 呢個公告正好係 OpenAI 部署下一代主要模型家族嘅時候，令人質疑成個研究係咪為咗市場推廣，而唔係為咗科學嚴謹性 。

究竟代表啲咩？

如果呢啲證明最後真係通過專家審查，咁多個結果將會結束幾十年嚟嘅開放問題。最重磅嘅成就——首次顯式構建非 sofic 群——解決咗一個超過 25 年嘅問題 。就連批評者都要承認，OpenAI 提供咗比一般企業公告多好多嘅可查驗材料 。

不過，最終嘅核心問題唔係「Astra 識唔識做數學」，而係：喺一個狹窄、形式化、可驗證嘅領域入面解決問題，到底可唔可以擴展到一般性嘅科學推理？答案暫時係：未有定論。