他證不出那個引理,換了個說法之後,AI 三秒就證完了

他證不出那個引理,換了個說法之後,AI 三秒就證完了

發布於
·21 分鐘閱讀
AIAI Agent產業觀察投資VC開源商業職涯創業產品

TL;DR

  • 多倫多大學數學教授 Daniel Litt 認為,目前最讓他佩服的 AI 自主成果是五月中公布的單位距離問題解答:大家本來以為那個猜想是對的,AI 找到了反例,而且用了六〇年代另一個領域的古典技巧。
  • 模型的推理過程「很像人」,不像 AlphaGo 那種外星棋步。而且各大實驗室主要 scaling 的是自然語言推理,不是形式化證明語言,這意味著這套進展很可能會外溢到數學以外的領域。
  • 模型強在不會累、記得多、能硬幹長計算、能把幾十篇論文的技巧拼起來。弱在直覺、大局觀、建立新理論,以及判斷「什麼問題值得問」。
  • 他做了十年的那些猜想,AI 幫不上忙,因為那些猜想大概是真的,沒有「造個反例」的捷徑可走。
  • AI 產出的證明之所以都很短,Litt 的判斷是因為長的它自己驗不了。已經有人丟出八百頁 AI 生成的論文,沒有人讀,模型也檢查不動。
  • 學術界正在出現「拉霸機模式」:博士後開著 agent 一小時刷出三篇正確但毫無價值的論文,同一個定理同一套證明在幾天內冒出四五篇。
  • 他最擔心的不是模型變強,是人類把理解外包出去之後,那個支撐整個前沿的人才輸送帶會斷掉。

這集是 a16z Podcast 在二〇二六年九月一日播出的訪談。a16z 是矽谷最有名的創投之一,這個節目基本上是他們的公開情報站,什麼題目都聊。這集的主持人是 Lisha Li,她今年剛加入 a16z 當合夥人,專門看前沿模型那一層的投資,在那之前自己創了一家生成式 AI 公司 Rosebud AI 做了八年,博士是在柏克萊念的,一開始念數學後來轉去做深度學習,所以她問問題的角度跟一般主持人不太一樣。

來賓 Daniel Litt 是多倫多大學的數學教授,研究領域是代數幾何和數論。他之所以在這個題目上有發言權,除了本身就是還在解問題的第一線研究者,更因為他過去一年多在網路上持續公開自己對 AI 的看法,而且看法一直在變。他在二〇二五年三月還跟人打賭 AI 到二〇三〇年做不出頂級論文,讓了三比一的賠率,現在他自己預期會輸掉這場賭。一個公開改變立場、而且把改變過程留在網路上的人,講的東西通常比較可信。

那個成果好在哪裡

過去一年 AI 解數學題的新聞多到看不完,但對外行人來說,每一則看起來都差不多,很難分辨哪些是真的重要。Litt 給了一個很好用的判準:看它後來有沒有被別人拿去用。

他最喜歡的是五月中公布的單位距離問題(unit distance problem,研究平面上一堆點彼此之間距離配置的老問題)解答。這件事有三層好。第一,圈內人本來普遍相信那個猜想是對的,結果 AI 找到了反例,方向本身就出人意料。第二,它用的技巧來自另一個領域,是六〇年代的古典想法,談不上多深奧,但對研究平面點配置的人來說是全新的。第三,也是最關鍵的,事後有一群數學家拿著這套想法去打掉了其他好幾個開放問題,包括實數上的和積猜想(sum-product conjecture)。

換句話說,判斷一個成果的價值,看的不是它當下有多轟動,而是它有沒有替後面的人開一扇門。Litt 說這是他目前唯一知道符合這個標準的 AI 成果。

至於前幾天剛出來的秩三十橢圓曲線(原本紀錄是二十九),Litt 的評價務實到有點掃興:很酷,但方法還沒公開,沒辦法評估。而且這類紀錄型結果在數學界的歸宿通常是「某人網站上的紀錄表」,不會進頂級期刊。

模型的思路,讀起來很像一個累不死的同行

主持人本來用「非人的」來形容 AI 的推理,Litt 當場糾正她:那個推理過程其實非常人類。OpenAI 放出的思考摘要,他讀起來就像自己解題時腦子裡跑的東西。沒有什麼 move 37 那種讓全世界棋手看不懂的招數,就是一個人類數學家在做數學,只是不會累、記得比較多。

這裡有個很多人沒注意到的技術細節,我覺得是整集最有商業意涵的一句話。各大實驗室主要在 scaling 的是自然語言推理,不是 Lean 那種形式化證明語言。很多人說「數學是可驗證領域,所以 AI 進步快」,但如果真正在 scale 的是非形式化的推理,那這套進展就沒有理由停在數學。Litt 的判斷是,技巧大概率會外溢到其他領域。

至於 Claude 跟 ChatGPT 的差別,他的答案很無聊也很誠實:能力上差不多,常常是一個解得出來、另一個也解得出來,或者兩個都卡住。他自己主要用 ChatGPT,理由是習慣,加上 ChatGPT 在數學上早一步變得可用。他還補了一句:兩邊的 theory of mind(心智理論,判斷對方知道什麼、不知道什麼的能力)都很爛。

強在應用,弱在提問

Litt 對模型能力的拆解很乾淨。強的部分:把已知技巧用到極致、硬幹超長計算、把散落在幾十篇論文裡的技術拼起來。他特別強調這不是貶低,歷史上有很多數學家靠這種能力做出了很好的職業生涯。

弱的部分是直覺跟大局觀。他描述自己的工作方式:先有一套非常不嚴謹的哲學,覺得這個東西跟那個東西有點像,然後花好幾年把這個「有點像」變精確。他的整個研究都建立在代數簇的上同調跟基本群表示之間的某種類比上。這種東西沒有一道題目,沒有標準答案,就是有人某天注意到「這兩邊長得很像」,然後三四十年的漂亮數學從那裡長出來。

模型目前在這一塊,用他的話說,自主做的話完全不行。給提示的話可以做出點有意思的東西,但那時候你就分不清哪部分是模型的、哪部分是你的了。他的觀察是:如果現在需要一百個位元的提示才做得到,六個月後大概就不用提示了。他不是能力停滯派。

還有一個更根本的弱點:搞清楚該問什麼問題。他舉了 Birch and Swinnerton-Dyer 猜想的例子,這是千禧年七大難題之一。它的來源是六〇年代兩個人用電腦跑出一堆橢圓曲線的統計數據,畫成圖,然後注意到某條線的斜率跟一個他們認識的代數不變量有關。這是史上最早用電腦輔助的數學之一,本質上是在做科學實驗。網路上那些開放猜想清單,其實遠遠沒有涵蓋「我們不知道什麼」。找到值得寫下來的猜想,往往比證明它還難。

他證不出來的那次,反而拿到了更好的東西

這集最精彩的故事在中段。

Litt 有篇論文裡有幾個引理他不滿意,覺得不夠好。其中一個引理,當時所有前沿模型都證不出來。於是他自己動手算了一大堆例子,算著算著突然想到:也許這件事之所以成立,是因為某個更根本的原因。他因此找到了一個更好的敘述。而一旦有了那個更好的敘述,模型很快就把它證完了。

後面才是重點。他事後把原本那個引理丟給 ChatGPT 5.6 Pro,它給出了一份十頁的證明,他形容是「你這輩子看過最爛的證明」,純粹是暴力計算,零洞見。那份證明完全正確,完全可以用,但如果他一開始就拿到它,他永遠不會發現後面那個漂亮的概念性解釋。

而他之所以沒有自己去硬幹那十頁計算,坦白說就是因為他懶得算。人類算不動、受不了、沒耐性,這件事在這個場景裡直接變成了優勢。

我覺得這是整集最值得所有行業的人抄下來的一段。之前在連手寫一個 HTTP 請求都不會了那篇提過工程師技能萎縮的焦慮,這裡講的是同一件事的另一面:卡住的那段時間,本身就有產出。如果每次一卡住就交給機器暴力通過,你會拿到答案,但那個「為什麼」永遠不會出現。

學術界已經出現拉霸機

Litt 做過一個實驗。他打開 codex,跟它說:上網找五個最近的代數幾何猜想,把它們證明出來。來回搞了一個小時,他拿到三篇正確的論文。品質很爛,但正確。它們現在躺在他硬碟裡,等他哪天想起來要寄信給相關的人。

他自己說這不是他時間的好用法,但問題是對別人來說可能是。一個正在找教職的博士後,未來一兩年在社群反應過來之前,最有效率的策略就是開著 agent 拉霸,拉到出一個可能正確的舊猜想證明為止。連要證哪個定理都不用先想。

現實中已經看得到後果。arXiv 上論文數量暴增,大部分不有趣,而且出現過同一個定理、同一套證明、四五篇論文在幾天內先後上傳的狀況,因為模型的推理路徑 mode collapse 在同一條線上。這是 Jimmy McGill 式的操作:每一步都在規則之內,組合起來就是在鑽學術體制的漏洞。

Litt 特別澄清一件事:這些低品質產出很多來自專業人士,因為學術界本來就有「多產」的激勵。反倒是非專業愛好者湧進來這件事,他覺得是好事,有更多人為數學興奮沒什麼不好。

順帶一提,這種「產出速度遠超過驗證速度」的失衡,在寫程式的世界早就上演過一輪,之前在一週合併六十個 PR,然後整個專案爛掉寫過,劇本幾乎一模一樣。

為什麼 AI 的證明都很短

有人稱讚 AI 產出的證明常常又短又漂亮。Litt 的解釋比較冷:因為長的它做不出來,或者說,做出來也驗不了。

模型現在的自我檢查能力已經比半年前好很多,你叫它產一個短證明,再問它「這對嗎」,它常常會誠實說不對。但東西一長,它就不知道自己錯在哪了。所以那些看起來優雅的短證明,比較像是能力邊界的形狀,而不是品味的展現。

他推測 OpenAI 跟 Anthropic 內部解掉的問題遠多於公布的,公布的那批之所以敢公布,很大原因是能用 Lean 形式化驗證。驗不了的那些,大概就留在內部了。

而 arXiv 上真的有人丟了八百頁 AI 生成的證明,聲稱解決了正特徵下的奇異點消解。Litt 說他沒讀,但那不可能是對的,因為那會是重大成果,超出現有模型的能力範圍。而且肯定沒有任何人類讀過它。

這裡他講了一件我覺得所有在用 AI 做審查、做 code review 的人都該知道的事:人類其實也不逐行檢查兩百五十頁的論文。人類的做法是理解整體論證結構,然後壓力測試它。這個論證是不是會推出某個我已知為假的東西?在這個特例下說得通嗎?他手上有一篇幾年前發表、其實錯了的論文,當年他跟一群同行一看就知道不對,因為它證出來的東西「強得不可能是真的」,但要找出具體錯在哪行花了好一番工夫。他拿這篇當測試,模型到現在都過不了:既找不出那個細微的錯誤,也做不到那種模糊的整體壓力測試。

順著這條線想下去,模型會被獎勵去鑽驗證機制的漏洞,其實是設計問題而非道德問題,這在模型那麼愛作弊,是因為教它的那套考題本身就是趕工寫的裡有更完整的討論。

一千個數學家,還是一個數學家複製一千次

Litt 對數學進展的看法是:它靠的是一群興趣各異的人各自追自己的好奇心,知識邊界因此在一個高維空間裡相對均勻地往外推,然後某天你會發現某個角落突然打通了一整片。

如果整個數學探索的方向被交給模型決定,而模型的推理路徑又高度收斂,那你得到的到底是一百萬個做著一百萬件事的數學家,還是一個數學家被複製了一百萬次?他沒有答案,但他認為這是各大實驗室該認真對待的問題。

然後他丟出一個更狠的假設:就算模型變成穩定超人,就算它自己也能提供足夠的認知多樣性,我們還是需要人類數學家。理由不是能力,是治理。一件事情最優,不代表它會發生。把方向盤交出去,沒有任何理由相信結果會是最優的那條路。他說如果你相信廣泛的基礎研究有價值,最保險的作法就是維持一個興趣夠雜的人類社群,讓他們去推著模型做這些事。

而且前沿那一小撮人,是靠底下成千上萬個學數學的人撐起來的。輸送帶斷了,前沿也沒了。

三歲的女兒跟正二十面體

聊到教育的部分很有意思。他觀察到課堂上開始出現雙峰分布:一群人真的搞懂了怎麼利用新工具,另一群人把作業丟給 AI 然後其他所有評量全部崩掉。制度調整的速度跟不上。

他自己的女兒三歲,沒用過 AI,會用手指數到三十,能加個位數。她學會的早期詞彙裡有一個是 icosahedron(正二十面體),因為祖父母送了她一個玩具。他說接下來要教加減法的時候,打算直接放在群的脈絡裡教。

他對女兒二十年後的世界沒有預測,但他認為教育的核心目的相當耐得住變化:學數學一直都是為了把事情想清楚、把世界看明白。就算身邊都是極強的 AI,這件事你大概還是會想做。

那句最該記住的話是他順口講的:數學的目的不是生產論文,是生產某種理解。如果那個理解最後住在模型權重裡,他覺得非常不令人滿意。把這句話裡的「數學」換成你自己的行業,大概也成立。


如果這種產業一線的實話你聽得下去,我持續在 wilsonhuang.xyz 寫這類筆記,訂閱一下就不會漏掉。

推薦閱讀

喜歡這篇文章嗎?

訂閱電子報,每週收到精選技術文章與產業洞察,直送你的信箱。

💌 隨時可以取消訂閱,不會收到垃圾郵件