OpenAI Astra 一口氣交十項數學成果，AI 原創研究去到邊一步？
成果有真分量，但十項當中有解決亦有推進，驗證同署名仍有爭議
OpenAI 今次交出嘅唔係數學比賽答案，而係十項涉及高維球體堆積、編碼理論、群論、量子複雜度、格密碼學同極值組合學嘅研究成果。官方話全部數學論證都由未公開模型 Astra 產生，人類協助整理成論文，模型再寫成 Lean 證書。呢個規模確實罕見，亦解釋到點解數學界今次反應遠大過以往啲跑分新聞。
十項成果，唔可以一律叫「解決十條難題」
OpenAI 自己而家用嘅字眼係十項成果各自「解決或大幅推進」長期未解問題。逐項睇，非 sofic 群嘅存在、Connes 剛性猜想、Ehrhart 體積猜想同幾條 Erdős 問題屬於聲稱解決或推翻；球體堆積、二元編碼、算術電路下界同最接近向量問題，主要係推高或收緊已知界限。後者可以好重要，但同徹底關閉一條問題始終差一截，所以「AI 一次解決十題」呢句唔準確。
The Verge 仲發現，OpenAI 最初話呢批問題至少十年冇實質進展，其後改成「解決或大幅推進長期未解問題」，頁面冇加更正說明。爭議最大嘅非 sofic 群成果，論文用到 Andreas Thom 同 Gábor Kun 喺 2016 同 2019 年發表嘅工作。OpenAI 後來承認相關論證依賴呢批較近期成果，反映真正難查嘅地方除咗答案啱唔啱，仲有模型究竟沿住邊批人類研究行到最後一步。
Lean 證書好有用，但唔係萬能封條
每項成果都有 Lean 證書，可信度高過淨係交一篇自然語言論文。Lean 核心會逐步檢查證明有冇跟足定義、公理同前置定理，少咗模型用流暢文字遮住邏輯缺口嘅空間。不過 Lean 官方文件講得好清楚：系統確認嘅係形式化命題有有效證明，唔會自動確認個命題準確表達原本想研究嘅問題。 用錯定義、漏咗條件或者引入有問題嘅前提，程式照樣可能接受一份內部一致嘅證明。
所以驗證要分兩層。電腦先檢查邏輯鏈，人類專家再核對形式化版本同原題有冇走樣、引用有冇漏、結果有幾新同幾重要。今批材料超過 250 頁，橫跨多個高度專門範疇，根本冇幾多數學家可以一個人審晒。OpenAI 願意公開論文、推理解說同 Lean 檔案係好事，但喺各範疇專家完成審閱之前，較穩陣嘅講法仍然係「有份量嘅候選成果」。
Astra 證明模型有能力自己解題，但要獨立做完整研究，仲有幾關要過。
Astra 展示到一種幾實在嘅自主解題能力：人類交低問題後，模型可以串連遠距離知識、試新構造，再寫出長篇論證。OpenAI 五月公開嘅 Erdős 單位距離猜想反例仲有外部數學家審閱，證明模型有機會提出人類未諗到嘅關鍵連接。不過完整研究仲包括揀問題、判斷邊條路值得追、追查文獻、解釋結果同建立新理論框架；今次公開資料未證明 Astra 可以長期包辦呢一整套工作。
揀中十個成功案例亦帶來選擇偏差。OpenAI 估算產生最終答案所用 token，按 Sol API 價計約 2,000 美元，但冇交代之前試過幾多題、跑過幾多次失敗嘗試。另一邊，Riemann-Bench 用 25 條有已知答案、由專家保密編寫嘅研究級問題測試前沿模型，全部得分都低過 10%。即係話，頂級內部模型偶爾可以做到重大突破，但未算每次遇到唔同研究題目都交到貨。
數學家嘅工作會先由驗證同選題開始轉
短期最明顯嘅改變，係證明草稿同探索速度會快好多，專家時間就移去設定問題、檢查前提、追來源同解釋新結果。博士訓練會幾尷尬：一個四年研究題目，而家睇落夠難，畢業前可能已俾模型攻破；學生如果一開始就攞答案，亦會少咗喺撞板過程建立直覺嘅機會。大學要教嘅會包括點驗 AI 證明、點披露工具參與，同點保留真正理解。
今次已足以叫數學界認真改工作方法，但「接管」仍然行得太前。下一步要睇各項論文經獨立專家審閱後剩低幾多、其他團隊可唔可以重現同類成果，仲有公開模型能否喺冇人挑選成功案例嘅情況下，持續處理全新研究問題。
參考來源
- The Verge — The AI takeover of mathematics has begun — original report
- OpenAI：Ten advances in mathematics and theoretical computer science — 核對十項成果分類、Astra、Lean 證書、論文整理方式同成本宣稱
- OpenAI：An OpenAI model has disproved a central conjecture in discrete geometry — 核對 Erdős 單位距離成果、外部數學家審閱同自主解題宣稱
- Lean 官方：Validating a Lean Proof — 釐清 Lean 可以驗證邏輯證明，但仍依賴命題翻譯、前提同函式庫可信度
- Riemann-Bench: A Benchmark for Moonshot Mathematics — 提供研究級保密題目嘅獨立測試結果，補充模型穩定能力嘅背景
- Leiden Declaration on Artificial Intelligence and Mathematics — 數學界對 AI 研究署名、公開科學、人類責任同教育影響嘅原則文件
本文根據原文及公開資料整理；資料有出入時，以原文及官方資料為準。
