作者：默思編輯部 發布：2026-08-31
2026年8月1日，OpenAI宣布其下一代模型Astra（目前尚未對外正式發布）產出了10道數學與理論電腦科學懸案的解答，這些題目都是懸置十年以上未解的問題。最受矚目的成果之一，是Astra明確構造出一個「非索菲克群」（non-sofic group），這是自1999年Mikhail Gromov提出索菲克性概念以來就懸而未決的問題。Astra同時反證了Connes剛性猜想，構造出無限多個彼此不同構、卻共享同一個von Neumann代數的性質(T)群，並證明了Ehrhart體積猜想，另外還在極值圖論領域解出兩道Erdős問題的反例。
過去AI模型宣稱「解出數學難題」時，外界常質疑證明的正確性只能靠人工審查，難以完全信任。這次OpenAI的做法不同：他們發布了一份249頁的手稿，並將所有證明轉換成Lean 4這套形式化證明語言撰寫的證明憑證，公開在GitHub上，採用Apache 2.0授權。Lean的核心驗證器（kernel）只會回傳「編譯通過」或「編譯失敗」兩種結果，是二元判定，不需要信任模型本身的說法。目前這份程式碼庫裡代表「尚未完成」的sorry計數是零，代表十道題目的每一個證明步驟都已完整驗證通過。
經營Erdős問題資料庫erdosproblems.com的曼徹斯特大學數學家Thomas Bloom在社群平台上表示這是「重大新聞」。整個過程的總推論成本，OpenAI估計約為2000美元，相較於過去數學研究動輒需要數年人力投入，這個成本效益比引發廣泛討論。
這次事件的意義不只在於解題本身，而是展示了「AI生成猜想與證明、形式化語言負責驗證」這套流程的可行性。未來如果類似模式普及，數學研究可能會出現新的分工型態：AI負責產生候選證明，人類數學家負責篩選有意義的方向與詮釋結果的重要性。
過去幾年不少AI公司都曾宣稱模型「解出」奧林匹亞級數學題或大學程度證明題，但外界質疑聲音始終存在，主要原因是這些宣稱通常缺乏可獨立驗證的完整證明過程，只能仰賴模型輸出的自然語言敘述，人工審核既耗時又可能有疏漏。這次Astra直接產出可被機器驗證的Lean 4形式化證明，等於是把「證明是否正確」這件事從仰賴信任，變成可以用工具直接驗證的客觀判定，這也是這次成果被視為分水嶺的關鍵原因。
形式化驗證（formal verification）技能過去主要用於晶片設計與關鍵軟體系統，隨著AI輔助證明興起，具備Lean、Coq等證明語言背景的人才需求可能會逐步擴大到數學研究與AI安全領域。