AI「生肉證明」堆爆GitHub！陶哲軒重磅發聲：只會解題沒用了

新智元報道

編輯：犀牛

【新智元導讀】陶哲軒最新判斷，數學正在從「證明稀缺」進入「證明過剩」時代——數學家最值錢的工作已不再只是「做出證明」，而是驗證它、消化它，并把一塊 AI 吐出的「生肉證明」變成人類真正吃得下的知識。

最近，陶哲軒在 Mastodon 拋出一記重磅判斷——

數學正在從證明稀缺時代，進入證明過剩時代（from an era of proof scarcity to an era of proof abundance）！

在AI對Erd?s問題的貢獻Github頁面上，20多份 AI 提交的全部或部分解，正堆在「pending assessment」（待評估）那一欄。

而在此之前，這個分類常年只有1-2份。

一夜之間，AI 正在以令人窒息的速度瘋狂輸出數學證明。

問題是——沒人來得及看。

問題求解「三件套」

生成、驗證、消化

陶哲軒把這次的思考建立在一個簡潔的框架上。

他說，數學問題求解從來不是一件事，而是三件事：

• Proof generation（證明生成）：把一個猜想從「未解決」推到「有解」。

• Proof verification（證明驗證）：確認這個解是對的，邏輯沒有漏洞。

• Proof digestion（證明消化）：把證明讀懂、講透、提煉出方法論，讓整個領域受益。

在過去的幾百年里，三件事基本由同一撥人完成——你證了一個定理，你自然理解它，你寫論文解釋它。

這三個環節之間不存在「瓶頸差」。

但 AI 來了之后，情況變了。

生成環節被 LLM 大幅加速，驗證環節有 Lean、Coq 等形式化工具兜底，唯獨消化環節——那個需要人類大腦去理解「這個證明到底意味著什么」的環節——完全跟不上。

陶哲軒用了一個精確的工程術語來形容這種錯位：impedance mismatch（阻抗失配）。

三個環節的速度不匹配了：證明像洪水一樣涌來，但理解的堤壩還是手工砌的。

他說，想象兩種社會。

食物稀缺的社會，最受尊敬的人是獵手和農夫——是那些「bring home the bacon」（把食物帶回家）的人。

你獵回一頭鹿，不管肉質如何，整個部落都會感激你，會有人主動幫你清洗、烹飪、分配。幾乎任何沒有毒的食物貢獻都受歡迎。

食物過剩的社會則完全不同。

想象一個 pot-luck 派對（每人帶一道菜的聚餐）。如果一個陌生人闖進來，扔下一塊來路不明的生肉，讓大家自己去處理——沒有人會高興。

甚至超市買來的預包裝食品，也只是勉強算數。

真正受歡迎的，是社區里受信任的成員精心烹制的家常菜——不僅因為好吃，更因為圍繞這道菜的對話本身就是社交的一部分，也是培養下一代廚師的機會。

回到數學——AI 跑出來的「生肉證明」（raw proof），就是那塊被陌生人扔在派對上的神秘肉。

它可能是正確的。它可能通過了形式化驗證。

但沒有人清洗過它、烹飪過它、也沒有人能告訴你它到底好不好吃。

陶哲軒直言：這種「貢獻」不僅沒有推進問題的實際進展（do not measurably advance the progress），反而可能產生一個「負面效果」——它殺死了人們繼續研究這個問題的興趣。

問題被宣告「已解決」了，但沒人懂這個解。

好比一道菜被端上桌，但沒人敢動筷子。

于是這道菜——連同圍繞它可能產生的所有對話和靈感——就這樣涼了。

Erd?s #1196，唯一跑通「三件套」的案例

理論都需要一個切片去檢驗。

陶哲軒反復提到的那個切片，就是 Erd?s 問題 #1196。

這是一個關于「primitive sets」（本原集）的猜想：在一個整數集合中，如果沒有任何元素整除另一個元素，那么對所有元素 a 按 1/(a·log a) 求和，當集合元素趨于無窮大時，這個和是否趨近于1？

1968年，Erd?s、Sárk?zy 和 Szemerédi 提出了這個猜想。

此后將近60年，數學家們不斷逼近——斯坦福數學家 Jared Lichtman 花了數年證明了一個相關的上界（約1.399），但最終的漸近猜想始終懸而未決。

2026年4月的某個周一下午，23歲的 Liam Price 把這道題丟進了 GPT-5.4 Pro。

Price 沒有數學博士學位，沒有多年的專業訓練。他用的是一個20美元/月的 ChatGPT Pro 訂閱——任何人都能用的工具。

80分鐘。

模型走通了一條數學界忽視了近90年的路徑：用von Mangoldt 函數（一種經典的解析數論權重函數）結合馬爾可夫過程理論，構造出了一個全新的證明框架。

這個技術組合已經存在了幾十年，但從未有人想到把它用在本原集問題上。

證明出來了。

但如果故事到這里就結束，它只不過又是一塊「神秘肉」。

關鍵在于接下來發生的事：陶哲軒親自下場。

他在24小時內驗證了證明的核心思路，隨后將其擴展、重組、打磨，最終揭示出這個證明背后隱藏著一條更深層的聯系——整數解剖學（integeranatomy）與馬爾可夫過程理論之間一條此前未被描述的全新橋梁。

這就是證明消化（proof digestion）。

不只是「對不對」的問題，而是「它意味著什么」的問題。

陶哲軒稱 #1196 是目前唯一一個三階段——生成、驗證、消化——都基本跑通的案例。

也正因如此，他反復強調一個原則：理想狀態是同一撥人完成全部三件事。

而現實中，越來越多的人在用 AI 生成證明后，沒時間去驗證和消化，就直接提交了。

這正是 Erd?s 問題近20多份待評估方案堆積的直接原因。

三處表態，同一判斷

陶哲軒不是在一個地方隨口說說。

他在幾乎同一時期，通過三個不同渠道發出了同一個信號。

4月27日，Mastodon 長帖：正式提出「證明稀缺→證明過剩」的范式判斷。

4月27日，Nature 訪談（The job description is changing）：他對記者 Davide Castelvecchi 說，數學家的「崗位描述」正在改變。一個拒絕碰 AI 工具、只想用傳統方式做證明的研究生，未來可能會發現自己的機會越來越少。

能在傳統數學功底之上熟練運用新工具的人，才會真正繁榮。

3月29日，博客長文《Mathematical methods and human thought in the age of AI》：他和 Klowden 花了超過一年寫成這篇論文，試圖超越眼前的技術細節，直面更根本的哲學問題——數學證明的本質是什么？論文的目的是什么？我們這個職業存在的意義是什么？

他在博客中寫道：如果我們自己不回答這些問題，它們就會被科技公司或經濟激勵機制替我們回答。

三處表態，同一個內核：數學家的核心競爭力正在遷移——從「誰先生成證明」，轉向「誰能選對問題、設計工作流、驗證并消化結果」。

稀缺的不再是答案，而是理解。

更大的震蕩：學術評價體系要重寫

如果只是數學家的工作方式變了，那還只是一個學科內部的事。

但陶哲軒看到的遠不止此。

當證明的成本被 AI 壓到接近于零，當證明驗證被 Lean/Coq 等形式化引擎大幅自動化——證明消化這個環節的價值就會被重估。

過去，消化證明是「免費的」。

你證了一個定理，你自然會理解它，會在論文里解釋它。這個勞動從未被單獨計價。

但當證明的生產者（AI）和理解者（人類）被拆開之后，消化就從隱性勞動變成了顯性稀缺資源。

這意味著整個學術聲望的分配邏輯要變。

Citation 體系、論文評審標準、獎項評選規則、甚至招聘和晉升的依據——所有這些圍繞「誰先證了什么」建立起來的激勵結構，都將面臨重構。

陶哲軒預測：就像現代社會不再把生食原料當作一頓飯一樣，數學研究文化將不再把「未消化的裸證明」（raw, undigested proofs）視為對一個問題的解決方案。

未來的評判標準，將聚焦于一個貢獻究竟在多大程度上豐富了整個領域，而非僅僅「解決」了問題本身。

而且這不只是數學一個學科的事。

AI for Math 的范式漂移，將成為所有強證明型學科的預演——理論物理中的計算驗證、密碼學中的安全性證明、軟件工程中的形式化驗證——所有依賴「正確性論證」作為核心產出的領域，都將面臨同樣的「阻抗失配」。

證明會越來越多，越來越快，越來越便宜。

證明的時代沒有結束。

但「證明即一切」的時代，正在落幕。

未來屬于那些不僅能「算出來」，更能「講明白」的人。

參考資料：

https://mathstodon.xyz/@tao/116477351524980995

https://mathstodon.xyz/@tao/116450581967483825

https://www.nature.com/articles/d41586-026-01246-9

https://terrytao.wordpress.com/2026/03/29/mathematical-methods-and-human-thought-in-the-age-of-ai/