OpenAI Astra 交出十項數學成果：識創新，定係識拼文獻？
證明過到 Lean，研究價值同可重複性仍要數學家核對
一次交十份成果，個量先令人震撼
OpenAI 8 月初公布，未公開模型 Astra 喺高維球體堆積、群論、量子複雜度、格密碼學同極值組合等範疇，交出十項新結果。官方用字其實留有空位：呢批工作有啲解決咗問題，有啲只係推前現有界限；類型亦包括新構造、反例同改良下界，唔適合統稱做「十條世紀難題全數破解」。The Verge 訪問多位數學家後，得到嘅大方向係成果相當有料，任何一項由年輕研究員做出，都足以成為重要學術工作。
五月嗰個反例，證據鏈暫時最完整
最容易睇清 Astra 能力嘅案例，其實係 OpenAI 五月公布嘅單位距離結果。模型用代數數論工具，構造出一批點陣反例，推翻數學界長期相信嘅 Erdős 上界猜想；Tim Gowers、Noga Alon 等外部數學家核對過論證，亦寫咗補充文章解釋點解個方法重要。要講準確啲，模型推翻咗一個主流猜想，未有求出整個平面單位距離問題嘅最終答案。不過佢搵到跨範疇連結，已經超出大型文獻搜尋器通常做到嘅整理工作。
有創新，同樣食盡前人研究
Astra 呢批工作顯示，模型識得重組舊工具、試冷門方向，偶爾仲會砌出專家冇諗過嘅構造；叫佢純粹搜尋器會低估咗成果。不過數學創新本身就建基於舊定理，要判斷成果有幾新，就要睇模型有冇交代來源，亦要同已有研究逐項比較。The Verge 指 OpenAI 最初聲稱相關問題至少十年冇進展，但論文內有一項明確沿用兩位研究員較近期嘅成果，官方之後修改咗說法。呢類問題未必等同抄襲，卻反映公司新聞稿嘅新穎性描述唔可以代替文獻審查。
Lean 證書好有用，但包唔晒成篇論文
OpenAI 話十項論證都有 Lean 證書，即係電腦可以按既定定義同公理，逐步檢查形式化證明有冇邏輯漏洞。呢層保障相當硬淨，不過 Lean 唔會判斷形式化命題有冇對準原本問題、假設有冇收窄，亦唔會話你知個成果係咪真係新。獨立研究者審查量子平行重複嗰章時，就喺印刷版證明搵到一個成功率同失敗率掉轉嘅錯誤；修正屬局部，原引理仍然成立，但作者亦講明，呢次修補冇獨立驗證後面成條主定理。所以有 Lean 證書之外，論文內容同學術價值仍要專家另外核對。
點解數學咁快成為 AI 示範場
數學問題邊界清楚，答案又可以用證明核對，模型於是可以大量試路，再用形式化工具篩走錯誤；生物、醫學或者材料研究仲有實驗、量度誤差同現實環境，冇咁容易靠運算閉環處理。OpenAI 話搵出十項解法所用 token，按 Sol API 價格計大約值 2,000 美元，但呢個數冇包括訓練模型、人類整理稿件、專家核對，亦冇公開一共試過幾多條失敗題目。欠咗呢個分母，外界只知道 Astra 成功過，仲未知道成功率有幾高，或者另一隊研究員可唔可以重做。
數學家嘅工作會移去揀題、解釋同驗證
研究人員日後最實際嘅用法，會係叫模型搵反例、比較幾條證明路線、補中間引理，再由專家判斷條問題值唔值得追、論證同文獻接唔接得上。呢個分工亦帶來一個幾現實嘅樽頸：生成二百頁證明可以好平，搵幾位真正識嗰個細分範疇嘅人逐頁核對就慢好多。對博士生同 STEM 學生嚟講，學識拆假設、查引用同驗證論證反而更重要；識問模型攞答案但冇能力驗貨，只會將錯誤稿件同審稿壓力一齊放大。
下一步要睇 Astra 可唔可以俾外界重做
Leiden Declaration 同國際數學聯盟要求透明、正確署名、獨立核對，同清楚交代人機分工，正好點中今次爭議。Astra 仍未公開，OpenAI亦冇披露揀題方法、失敗次數、prompt、人類中途提示同總運算成本，所以由十項成果推論 AI 已經可以全面取代數學家，步子跨得太大。較可靠嘅判斷，要等各範疇專家完成同行評審，再睇其他團隊能否用唔同模型重現同級成果。
參考來源
- The Verge — Welcome to the AI crisis in math — original report
- Ten advances in mathematics and theoretical computer science — OpenAI 官方公布十項成果、Astra 身份、Lean 證書同 token 成本說法。
- Ten Advances in Mathematics and Theoretical Computer Science — 十項成果嘅完整技術稿件，用嚟核對每項工作屬於證明、反例、構造定界限改良。
- An OpenAI model has disproved a central conjecture in discrete geometry — 單位距離反例嘅官方資料，亦列出參與核對嘅外部數學家同補充論文。
- Auditing an AI-Generated Mathematical Proof: A Correction to a Greedy Conditioning Lemma in Quantum Parallel Repetition — 獨立審查指出量子平行重複章節嘅局部證明錯誤、修正方法，同修正未能驗證主定理嘅界線。
- Leiden Declaration on Artificial Intelligence and Mathematics — 數學界就 AI 研究提出嘅透明度、署名、獨立驗證同人類責任原則。
- IMU News 137: The IMU endorses the Leiden Declaration — 國際數學聯盟解釋點解支持宣言，亦交代形式驗證、同行評審同研究自主嘅風險。
本文根據原文及公開資料整理；資料有出入時，以原文及官方資料為準。
