OpenAI Astra評測：砸2000美元解開10道數學懸案 | OpenAI Astra Review: AI Solves 10 Unsolved Math Problems
By Kit 小克 | AI Tool Observer | 2026-08-08 🇹🇼 OpenAI Astra評測：砸2000美元解開10道數學懸案 OpenAI Astra 是OpenAI下一代旗艦模型的內部代號，8月初一次丟出震撼彈：用它解開了10道懸而未決超過10年的數學與理論電腦科學難題，總運算成本只花了約2000美元（以GPT-5.6 Sol API計費）。這則消息在Hacker News、X和數學圈同步發燒，因為過去AI「解數學題」通常是套用已知方法算得快，這次不一樣——是產出人類還沒證出來的新結果。 Astra到底解出了什麼 OpenAI公布的10個成果橫跨高維幾何、編碼理論、群論、量子複雜度、格密碼學、算子代數與極端組合數學。其中最受矚目的三項： 非可及群（non-sofic group）的顯式構造 ——這是Mikhail Gromov在1999年提出可及性概念以來懸而未解的問題 推翻Connes剛性猜想 ，這是馮紐曼代數領域的重要猜想 高維球堆積密度 的新上界，把1978年就沒進展的紀錄往前推進到Cohn-Elkies門檻 此外還解出了Erdős問題183（多色Ramsey數）等三道Erdős問題目錄裡的題目。 怎麼確定不是幻覺出來的假證明 這才是Astra這次公告真正值得注意的地方：OpenAI沒有只丟一份249頁的手稿，而是同步釋出 Lean 4形式化證明 ，放在GitHub上以Apache 2.0授權公開，整個repo的「sorry」計數是零——代表所有10道證明的每一步都經過機器驗證，不是模型自己說了算，也不需要數學家肉眼一步步覆核每個推導。這對「LLM會一本正經編造證明」的長期質疑，算是給了一個可驗證的回應。 誠實看待：這代表什麼、不代表什麼 先講清楚： Astra還沒有公開發布 ，一般人現在用不到。這次公告更像是OpenAI在為下一代模型的正式上市鋪路，挑的10題也是精心挑選過、已知「有機會被推進」的方向，不是隨機出一道題目給AI解。換句話說，這不等於AI已經能像數學家一樣「自主研究」，比較接近在特定、範圍明確的形式化系統裡，高效率地搜索與組合已知技巧。但形式化驗證這一步做得紮實，值得數學圈認真看待，而不是又一次「AI又要取代誰」的行銷話術。 好不好用，試了才知道 🇺...