陶哲軒驚呼“變天”，AI用6小時改寫數(shù)學史

一塊閃亮的數(shù)學獎牌，剛剛被寫入代碼的智能體在6小時內摘下，而人類為此思考了30年。

PART 01

AI六小時破解30年數(shù)學難題

2025年12月，人工智能領域迎來里程碑事件：Harmonic公司開發(fā)的AI系統(tǒng)“亞里士多德”僅用6小時便攻克了困擾數(shù)學界30年的埃爾德什問題#124簡化版。這一突破被學界稱為“數(shù)學智能體時代的開端”，而菲爾茲獎得主陶哲軒則犀利指出：AI正在高效收割數(shù)學界的“低垂果實”，讓人類研究者得以聚焦更具挑戰(zhàn)性的核心問題。

埃爾德什問題#124自1995年提出以來，一直是組合數(shù)論領域的頑固堡壘。其核心命題探討：給定k個不小于2的自然數(shù)d?，若∑1/(d?-1) ≥ 1，是否所有足夠大的自然數(shù)n都能表示為特定0-1組合的和？這個看似簡潔的問題，卻讓數(shù)學家們在最大公約數(shù)（gcd）約束和邊界案例驗證中陷入長達三十年的僵局。

“亞里士多德”的突破性在于其完全獨立的證明能力。它采用創(chuàng)新的“vibe proving”方法論，融合強化學習與蒙特卡洛樹搜索，在無需人類干預的情況下遍歷上億種證明路徑，最終輸出100%可驗證的定理。整個過程僅耗時6小時，而通過Lean形式化驗證系統(tǒng)的檢驗只需1分鐘。

耐人尋味的是，當通用AI巨頭ChatGPT和Gemini面對同一問題時，卻集體“折戟”。陶哲軒分析指出：Gemini僅能給出排除數(shù)字1后gcd條件成為必要的基礎觀察；ChatGPT則表現(xiàn)出明顯的“路徑依賴”，大量引用已有網(wǎng)頁和論文，未能提出原創(chuàng)性觀點。

這種差異揭示了專業(yè)AI與通用AI的本質分野——當“亞里士多德”被設計為“邏輯工匠”，基于形式邏輯生成可驗證代碼時，ChatGPT類模型仍是“猜詞機器”，依賴統(tǒng)計概率生成文本。

PART 02

“人機協(xié)同”的科研革命

陶哲軒將數(shù)學未解問題的分布描述為“長尾特征”。大多數(shù)難題并非超高難度，而是因人類數(shù)學家資源有限而被擱置的“低垂果實”。AI的自動化能力恰恰擅長處理這類問題。

在埃爾德什問題網(wǎng)站上，“未解”標簽最近減少了近十個，這并非因為人類突然解決了這些問題，而是AI通過文獻檢索發(fā)現(xiàn)它們早已被攻克。這種現(xiàn)象揭示了AI作為“清道夫”的價值——它能清理最容易解決的問題，讓人類聚焦于真正具有挑戰(zhàn)性的核心難題。

HarmonicMath創(chuàng)始人Vlad Tenev提出的“Vibe證明時代”已經(jīng)到來。這一概念意味著AI不僅能輔助驗證，還能獨立創(chuàng)造。在數(shù)學領域，這種變革尤為深刻，因為數(shù)學的形式化特性使其非常適合AI參與。

微軟前AI副總裁Sebastien Bubeck激動地分享道：“該解決方案100%由AI生成，總計耗時6小時。”這一效率與人類數(shù)學家30年的掙扎形成鮮明對比，凸顯了AI在科研效率方面的革命性提升。

PART 03

AI當前局限與信息學學生的不可替代性

盡管“亞里士多德”取得了突破，但它解決的是原問題的簡化版本。原版埃爾德什問題#124不允許使用數(shù)字1且需要滿足額外的最小公約數(shù)條件，這一更復雜的版本仍有待解決。

AI在數(shù)學推理中面臨的主要挑戰(zhàn)之一是“超長推理鏈”問題。高中數(shù)學證明可能只需10到40步，而像黎曼猜想這樣的難題，證明路徑可能長達百萬步。美國加州理工學院的謝爾蓋·古科夫指出，這類超長路徑極難處理，AI必須在指數(shù)級增長的可能路徑中找到正確解法。

DeepMind的AlphaProof和AlphaGeometry2在國際奧數(shù)競賽中表現(xiàn)出色，但專家們普遍認為，它們仍缺乏真正的數(shù)學洞察力。競賽題有一定“套路”，而真正的數(shù)學研究更開放、復雜。初創(chuàng)公司Epoch AI的FrontierMath測試顯示，面對全新技術難題，LLM幾乎集體“交白卷”。

數(shù)學家董彬指出，AI在數(shù)學研究中的理想角色是“AI學徒”——用訓練數(shù)學家的方式培養(yǎng)AI助手。但目前，AI更適用于“單點突破”，從局部解決某些具體問題，而非全面替代人類直覺和創(chuàng)造力。

PART 04

信息學學生的四維能力重構

當AI開始收割數(shù)學“低垂果實”，信息學學生亟需重構能力模型，在以下四個維度建立新優(yōu)勢：

人機協(xié)同的架構思維——“亞里士多德”的成功源于其專業(yè)定位——與通用大模型不同，它專為數(shù)學證明設計，融合強化學習、蒙特卡洛樹搜索與Lean形式化語言。這種“領域專用智能”架構思維值得信息學學生深入學習。正如DeepSeek-V3.2-Speciale模型展現(xiàn)的，通過融合定理證明能力，專業(yè)模型在IMO、ICPC等賽事中已超越多數(shù)人類選手。

形式化驗證的必備技能——Lean證明系統(tǒng)的應用標志著數(shù)學驗證進入程序化時代。信息學學生需掌握形式化驗證工具，將自然語言證明轉化為機器可驗證代碼。這不僅是防范AI幻覺的有效手段，更是未來科研協(xié)作的基礎能力。埃爾德什#124的證明在GitHub公開后，全球研究者均可參與驗證與拓展（github.com/plby/lean-proofs）。

直覺引導的算法設計——當前AI在依賴性質觀察與解題直覺的題目上仍存在明顯局限。如AlphaProof解決3個IMO問題耗時3天，而人類選手僅需4.5小時。信息學學生應強化元認知能力，在AI陷入局部最優(yōu)時提供方向性指導，這正是人類思維不可替代的核心價值——正如PatternBoost AI系統(tǒng)開發(fā)者所言：“探索性思維是數(shù)學的核心”。

問題發(fā)現(xiàn)的戰(zhàn)略眼光——倫敦數(shù)學科學研究所何楊輝指出：AI能幫助證明問題，卻無法幫助確定需要解決的關鍵問題。信息學學生需培養(yǎng)科學發(fā)現(xiàn)的前瞻力，在AI清理“低垂果實”后，精準識別真正值得攻堅的“數(shù)學高峰”。這種能力建立在對學科發(fā)展脈絡的深刻理解與跨領域知識融合基礎上。

PART 05

教育轉型：從工具使用者到智能體架構師

面對AI的沖擊，信息學教育正在經(jīng)歷范式轉變。2025年CNCC論壇達成共識：信息學奧賽應繼續(xù)堅持以計算思維培養(yǎng)為核心，同時更加重視學生發(fā)現(xiàn)問題和提出問題的能力。微軟前AI副總裁塞巴斯蒂安·布貝克激動地分享AI攻克埃爾德什難題的消息時，強調“解決方案100%由AI生成”。

但走進普林斯頓高等研究院，數(shù)學家們已在全新實驗室工作：人類提出大膽猜想，AI負責驗證與反例生成；人類構建理論框架，AI完成繁瑣計算；人類捕捉靈感火花，AI將其轉化為嚴謹證明。