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

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

PART 01

AI六小時破解30年數學難題

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

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

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

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

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

PART 02

“人機協同”的科研革命

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

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

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

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

PART 03

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

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

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

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

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

PART 04

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

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

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

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

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

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

PART 05

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

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

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