AI小貼士

By Kit 小克 | AI Tool Observer | 2026-08-11 🇹🇼 Astra評測：OpenAI花2000美元解開10道數學懸案 Astra 是 OpenAI 尚未正式發表的下一代模型，8 月初它做了一件過去 AI 少見的事：用大約 2000 美元 的運算成本，產出 10 道數學與理論電腦科學界懸而未決超過十年的難題解答，還附上 249 頁手稿與可機器驗證的 Lean 4 形式化證明。這不是又一次「跑分刷新高」，而是 LLM 第一次被主流數學家認真討論「這算不算原創研究」。 Astra 解開了哪些數學難題？ 根據 OpenAI 公布的資料，Astra 這次交出的成績單包括： 首次明確構造出「 非 sofic 群 」（non-sofic group），解決自 1999 年 Gromov 提出 sofic 群概念以來、懸而未決近 27 年的問題 推翻 Connes 剛性猜想 （von Neumann 代數領域的重要猜想） 證明 Ehrhart 體積猜想 解出 Erdős 問題集 中 3 道題目，包括第 183 號多色 Ramsey 數問題 所有證明都上傳到 GitHub 的 openai/ten-proofs 倉庫，採 Apache 2.0 授權，Lean 4 的「sorry count」是 0——代表每一步推導都經過形式化系統逐行驗證，任何數學家都能自己下載檢查，不用相信 OpenAI 的一面之詞。 2000 美元的意義：便宜不代表灌水 過去用 AI 輔助證明數學定理的案例不少，但通常需要龐大算力或人工介入很深。Astra 這次用 GPT-5.6 Sol API 定價換算，10 道題目加起來只花 2000 美元，這個數字重點不在便宜，而在於證明「原創數學推理」正在變得可規模化、可複製。 爭議：Astra 有「抄」前人論文嗎？ Astra 的評測不能只看正面消息。菲爾茲獎得主 Timothy Gowers 公開表示，其中一項結果他會毫不猶豫推薦投稿頂級期刊，Erdős 問題集維護者 Thomas Bloom 也稱這是「大新聞」。但 Yeshiva University 數學家 Steven Miller 指出，Astra 的球體堆積證明疑似沿用他 2016 年論文的論證邏輯，卻沒有標註來源...

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又要取代誰」的行銷話術。 好不好用，試了才知道 🇺...