評論：AI 借 Lean 寫數學證明，不讀 AI 程式碼漸成常態
一位電腦科學家在這篇評論中指出，AI agent 結合 Lean 等互動式證明助手，正在把希爾伯特百年前設想的「證明機器」變為現實，其對數學界的衝擊甚至超過希爾伯特綱領的失敗。他同時警告，程式設計領域已把不讀 AI 生成程式碼當成常態；而在 Curry-Howard 對應下程式與證明本質相同，放棄閱讀就等於放棄理解。他主張像數學家反覆簡化 AI 證明那樣，用抽象、重構與更高層語言把程式碼簡化到能裝進腦中。
原標題：Wir müssen wissen – wir werden wissen
閱讀原文
| 評分 | 44 / 50（平均 47，門檻 76） |
|---|---|
| 狀態 | 未入選 |
相關報導
論文：Lean 驗證 AI 形式化證明不等於原證明正確
arXiv 新論文指出，用 Lean 機械驗證 AI 自動形式化的數學證明，並不能保證原始自然語言證明本身正確。作者 Bastounis、Circelli 與 Hansen 證明，要做到語義忠實的翻譯必須消解自然語言數學文字的歧義，而該問題在可解複雜度指數（SCI）層級中為無窮，比停機問題（SCI=1）更難。
數學家 Maggi 撰文：LLM 已生成數學證明，人類理解是關鍵
數學家 Francesco Maggi 發表長文評估 LLM 對數學的衝擊：LLM 已產出帶外力項 Navier–Stokes 方程的有限時間爆破解、準黎曼猜想的證明草案等成果，但人類能否理解這些結果，將決定數學走向「黃金時代」還是「黑暗時代」。他指出 LLM 最擅長寫 Lean 證明，重要定理的 Lean 版本可長達數十萬行，而機器生成的自然語言翻譯往往更亂、更不忠實，目前難以直接閱讀。他認為數學不會因機器能證定理而終結，社會反而需要更多數學家，並分八點討論相關選擇。
陶哲軒宣告數學 2.0 時代：AI 讓證明從稀缺走向氾濫
菲爾茲獎得主陶哲軒發布《數學 2.0》演講，宣告建立在證明稀缺之上的數學 1.0 時代落幕：AI 正讓數學證明變得氾濫。他呼籲建立更透明的評估機制，把失敗結果與算力成本一併納入報告，並減少對搶先生成證明的強調，轉而重視解釋、評審與知識整理；其參與創立的 SAIR 基金會開放數學模型計劃將很快發布。此番表態的背景是 OpenAI 一次性發布 722 篇數學論文後，陶哲軒牽頭成立人類數學協會（AHM），並呼籲數學家停止與 OpenAI 合作。
20 年經驗工程師撰文：AI 程式碼仍須逐行審查
一位寫了 20 年程式碼的軟體工程師撰文主張，AI 生成的程式碼仍要逐行讀、逐行審，不能因為能跑就盲信。他承認這類工具寫得比自己快，經審查後品質往往也不差，但它的做法主要是不斷做加法：堆砌覆蓋錯條件的單元測試、重複實現已有函式、每行都加無用註釋，出問題後還會編造一套語氣篤定的根因分析。他認為 95% 的正確率不等於 100%，靠提示詞“配方”解決不了問題，行業還缺少可重複的驗證流程；只要 PR 上署著自己的名字、自己還在值班，就該讀懂這段程式碼。
陶哲軒轉向 AI 減速派，呼籲模型公司放慢數學研究
數學家陶哲軒在 SAIR 演講中公開呼籲模型公司放慢數學研究節奏，稱 AI 無休止加速卻對後果一無所知，並稱之為 Proof Indigestion（證明消化不良）：AI 只在生成解答與 Lean 驗證上狂飆，理解、評審、寫入教科書幾乎停滯。此前他與 25 位菲爾茲獎得主聯名發表公開信，批評把數學當 benchmark 刷分。OpenAI 隨後回應，宣布在普林斯頓高等研究院設立數學與人工智慧顧問小組，但宣告寫明該小組不就數學上的內部進展提供建議。