多倫多大學數學家Daniel Litt稱AI長證明受制於驗證能力
多倫多大學數學家Daniel Litt表示，當前AI模型在數學上的關鍵瓶頸並非生成文字，而是無法可靠驗證複雜推導的正確性；模型可以寫出證明，卻未必知道證明在哪一步失效。
Litt稱，向模型索取較短證明後再追問其是否正確，模型常會自行否認或修正先前結論；但證明變得足夠長、包含大量定義、引理、分類討論和引用鏈後，錯誤可能被後續文本掩蓋，模型也缺乏穩定的全局一致性檢查能力。
他提到一份聲稱解決正特徵域奇點消解問題的論文，全文約800頁且由AI生成。該問題屬於代數幾何中的基礎難題：目標是在不改變對象雙有理結構的條件下，經由一系列操作將奇點轉化爲光滑結構；在特徵零情形已有經典結果，而正特徵情形仍包含高難度開放問題。
Litt稱自己尚未在這份800頁文本中定位具體錯誤，但認爲其不可能已構成有效證明：該結論若成立將是數學重大突破，而既沒有人類專家完整審閱，也沒有現有模型具備審計整份複雜證明、追蹤所有依賴關係並獨立確認結論的能力。
該判斷與Litt此前對AI數學能力的立場形成反差。他曾就AI能否在2030年前獨立寫出達到2025年《Annals of Mathematics》水準的數論論文下注，並在AI已展示對部分數學問題的實質性進展後提前承認判斷失誤；但他仍將“可驗證的長鏈推理”視爲從局部解題走向自主數學研究的分界線。
市場機制上，資金會優先流向形式化驗證、定理證明器、證明搜索、代碼驗證、科學計算與高質量訓練數據基礎設施，而非單純追逐能輸出更長推理文本的模型。受益方包括能將模型生成結果接入Lean、Coq、Isabelle等可機器檢查體系的開發者，以及擁有數學、工程和科學驗證數據的機構；承壓方是將自然語言AI輸出直接包裝爲科研結論、金融模型或安全關鍵代碼結論的產品，因爲其責任成本將隨着錯誤難以審計而快速上升。
來源：公開信息
ABAB AI 解讀
數學史上，“提出猜想”和“給出可審計證明”一直是兩種完全不同的能力。Andrew Wiles在1993年公佈費馬大定理證明後被發現存在關鍵缺口，隨後與Richard Taylor用近一年時間補全；Grigori Perelman提出Poincaré猜想證明後，數學界也花費多年組織專家覈驗與整理。Litt的800頁例子處在同一邏輯下：長文本不是證明強度的信號，反而提高了局部假設錯配、符號漂移、隱含前提遺漏和引理循環引用被漏檢的概率。
資本路徑正在從“生成能力”轉向“驗證閉環”。大模型公司可用論文、教材、代碼和合成推理軌跡訓練模型提出候選證明，但最終產品化需要把候選答案編譯到可檢查的形式系統中：模型負責搜索、拆分子問題與生成形式化草稿，定理證明器負責判定每一條推導是否滿足公理和規則。這個路徑與軟件工程中GitHub Copilot到靜態分析、單元測試、持續集成和形式化驗證的演化一致——生成代碼的邊際成本下降後，測試、審計與責任歸屬成爲稀缺資源。
行業類比最接近AlphaGo到AlphaFold的差異。圍棋有明確規則和勝負判定，模型可以通過自我對弈得到高質量反饋；蛋白結構預測則可以用實驗結構數據評估，但預測結果仍需實驗驗證。開放數學介於兩者之間：形式化後的命題可由證明內核做二元檢驗，但把真實數學語言、定義與研究方向完整翻譯進形式系統，仍需要昂貴的人類專家工作。當前模型處在“生成候選路線和局部步驟”的擴張階段，尚未進入“端到端、自動產出並自動認證重大理論”的控制階段。
本質屬於定價權轉移。模型把寫作、檢索和局部推導變成低成本能力後，可信度不再由誰能寫出最長的證明決定，而由誰控制驗證系統、形式化語言、權威數據集和專家審稿網絡決定。生成端的供給會爆炸，驗證端的人力、工具和注意力卻相對稀缺；因此AI越能快速製造複雜結論，獨立覈驗的成本越高，驗證基礎設施的價值越可能向少數擁有工具鏈與標準制定權的平臺集中。
ABAB News · 認知定律
能生成答案，不等於能承擔答案
信息越廉價，驗證越成爲稀缺資產
複雜度不是壁壘，可信驗證纔是壁壘