★置頂zzllrr小樂公眾號，追蹤《小樂數學科普》系列報道！

劍橋大學女王學院21歲本科生凱文·巴雷托（Kevin Barreto）受邀講述首個被正式認可、由AI人工智能原創解決埃爾德什問題（即第728號問題）的來龍去脈。

凱文·巴雷托（Kevin Barreto）

作者：Kevin Barreto（凱文·巴雷托）2026-1-26

譯者：zzllrr小樂（數學科普公眾號）2026-5-20

求喜歡

作者自述

嗨！我是一名21歲的英國學生，目前在劍橋大學女王學院攻讀純數學專業，大二。我對篩法和解析數論很感興趣，尤其關注 L函數，例如黎曼 zeta 函數。我最初申請的是劍橋大學三一學院，但很遺憾被拒。幸運的是，女王學院基于我的社會經濟背景和考試成績重新考慮了我的申請。由于長期與抑郁癥作斗爭，我不得不休學一年，重讀大一。

托馬斯?布魯姆（Thomas Bloom，埃爾德什問題集網站 erdosproblems.com 站長）盛情邀請我，講述首個被正式認可、由AI人工智能原創解決埃爾德什問題（即第728號問題）的來龍去脈。我也想在文末簡要談談我對當前數學領域人工智能發展方向的看法。

題目回顧

埃爾德什第728號問題（已獲證明、Lean形式化）

設 C>0 與 ?>0 為充分小的常數。是否存在無窮多組整數 a,b,n，滿足 a≥?n 且 b≥?n，使得a!b! 整除 n!(a+b?n)! 并且 a+b > n + C log n？

這是埃爾德什、格雷厄姆（即葛立恒）、魯茲薩與斯特勞斯提出的問題。埃爾德什證明了：若 a!b! 整除 n!，則 a+b ≤ n + O (log n)。

該問題可改寫（令 k = a+b?n，N = a+b）為：是否存在無窮多組滿足條件的整數，使得組合數 C(N,k) 整除 C(N,a)。

本問題表述存在歧義，按字面寫法存在若干平凡解。例如 AlphaProof 團隊指出，存在 a 與 b 極大的解，比如取a = n+w+1，b = (n+w+1)!/n! ? 1，其中 w ≥ max (C log n, ?n)。

根據上下文推測，原題本意應包含條件 a,b ≤ n，但即便如此仍存在平凡解，例如取 a=b=n，或 b=n?1 且 a 為 n 的任意大因子。顯然作者本意應包含類似 a,b ≤ (1??) n 的約束。

巴雷托與ChatGPT-5.2證明了：對任意 0 。

該結果按原題本意回答了該問題。

研究背景

從13歲起，我就主要對解析數論抱有濃厚興趣。我知道埃爾德什問題已有數年，但一直不覺得自己能做出什么有分量的貢獻。我之前瀏覽過這些公開問題，基本都不知道從何入手。

2025年11月，有消息稱Harmonic公司的Aristotle系統解決了埃爾德什第124號問題的簡化版本。看到這條消息時，我的想法略有轉變。當時我還不太相信人工智能系統的能力，但我覺得，如果這類系統能在這些問題上取得進展，那或許存在一些 “低垂的果實”，我也能為之貢獻一份力量。

受此鼓舞，我后來決定重新瀏覽數論領域的公開問題，尋找那些看起來足夠初等、本科生也有可能解決的問題。我最終偶然看到了第481號問題，并立刻想到了一個可能可行的思路。（唉，當時我太天真，嘗試解決這些問題前沒有去檢索文獻。）

我拿出iPad把思路寫下來，寫完后基本確信自己得到了正確證明。但人總該起身走一走，用清醒的頭腦再檢查一遍。于是我起身離開房間，散步了半小時。回來時，我更加確信證明是對的。

但這是我第一次在這個網站發帖，聲望完全懸而未決。為了確保不會不小心出丑，我用 Lean4 對證明進行了形式化。雖然我覺得憑自己的Lean知識足以完成（證明本身很初等），但在大語言模型協助下會更快。這是人工智能在整個故事中第一次發揮作用：我很早就發現，在智能IDE環境里，Claude Opus 4.5是唯一一個勉強能寫Lean 4代碼的大語言模型，前提是你提示它持續在當前 Mathlib4 的GitHub倉庫里搜索有用的證明策略。

順帶一提，我是Aristotle早期測試組的成員，它最初還是iOS應用時我就參與了，也是最早獲得其API權限的人之一。但我印象中這次并沒有用到它，要么是當時還不可用，要么是我沒來得及測試，具體記不清了。

無論如何，我最終完成了第481號問題證明的完整形式化，并把非形式化證明連同Lean證明的鏈接發到了網站上。結果證明，我的解法確實正確。遺憾的是，后來有人指出該問題早已被解決，我對此毫不知情。我有點沮喪，但很快釋懷，至少這是一次有用的學習經歷。（好笑的是，后來我在第333號問題上又犯了同樣的錯誤，這事后面會提到。）

這次小成功之后，我有了足夠信心去嘗試更難一點的問題。我覺得西頓集（Sidon sets）很有趣，于是被第43號問題深深吸引。在給出一個小反例后，有人指出該問題應理解為對充分大的N成立。我不記得自己是如何得知博斯（Bose）與喬拉（Chowla）的結論的，但當時我已經知道這個結果，并覺得可以用它來解決第二個問題。果然，我最終構造出了無窮多組反例，就此解決了第43號問題的一半。

人工智能實驗

出于好奇，我一向喜歡把這些系統的能力逼到極限。我有一個持續了8個月的本科數學評測集（感興趣可以查看 https://pellaml.github.io/iumb/ ），用來測試大一、大二的核心內容，至今仍未被模型完全攻克。大約在這個時候，GPT-5.2 Thinking發布，我的評測顯示它在數學能力上遠超之前所有模型。我自己只用了一兩個小時，就迅速意識到它的證明撰寫能力比前代強得多。

我在大學圣誕假期初享受了短暫的成功喜悅。當月晚些時候，我好奇這些模型究竟進步到了何種程度，GPT-5.2是否達到了解決公開埃爾德什問題的水平。我預計它或許能解決某個 “低垂的果實” 類問題。

就在這時，我的Discord好友利亞姆（Liam）告訴我，他也想做類似測試。他有基礎數學背景，對人工智能在科學領域的進展很感興趣。我提議我們一起嘗試攻克公開數論問題，作為科學實驗，看看GPT-5.2能否解決其中任何一個。

我選擇數論的原因有三：第一，這是我背景最深厚的領域，足以判斷模型的嘗試是否合理；第二，初等數論是最古老的領域之一，擁有數百年的訓練數據；第三，這類問題的很多解法不算太抽象，容易用計算機驗證，適合強化學習。這些都讓我預判模型在初等數論上會表現更好，而我的評測結果也印證了這一點。

利亞姆和我輪流給模型輸入各種問題，看它能否取得進展。我主要挑選那些我覺得有希望解決的問題。我們很早就注意到GPT-5.2的一個特點：如果它發現某個問題是網上公開的研究問題，就會拒絕認真嘗試，只給出問題概述與已知文獻結果。于是我們形成了如下工作流程：

1. 給模型輸入問題，看它能否找到相關文獻或取得進展。

2. 新開一個對話，再次輸入問題，并加上類似提示：“這是一道復雜的競賽類數學題。求解并給出嚴格證明或反證。不要聯網搜索。” 這通常能 “騙過” 模型，讓它真正認真解題，對初等數論問題尤其有效 —— 這類問題很容易讓模型誤以為是奧林匹克競賽題，而它在強化學習中見過大量競賽題。

3. 如果模型給出解法，就要求它寫成可發表數學論文格式的 LaTeX 代碼塊，再把 TeX 文件交給 Aristotle 嘗試自動形式化。如果模型沒能給出解法，就用這樣的提示：“檢索埃爾德什第 X 號問題，理解其真實含義。然后提出可能導向正確證明或反證的新穎、創造性思路。最后寫一段簡短的 LaTeX 提示，讓大語言模型能用你選定的思路給出嚴格證明或反證。絕對不要提及這是埃爾德什問題或公開問題。” 之后回到步驟 1，希望它最終能給出看起來合理的解法。

4. Aristotle輸出結果后，可能需要重新運行幾次，在它生成的 Lean 文件基礎上繼續完善，每次都把 TeX 和 Lean 文件傳給它，因為它經常會用完計算配額。當得到完整 Lean 文件，且 Aristotle 在頂部注明已完成問題解法的形式化后，再檢查最終主命題是否準確，確保它證明了該證明的內容。如果通過，恭喜，模型就正確解決了這個問題！

我是Lean形式化的堅定支持者。我很早就明確告訴利亞姆，除非我非常確定AI生成的證明正確且已完成（或正在進行且必定完成）Lean形式化，否則我不會發帖。我不會讓在職數學家去翻閱一堆可能毫無價值的AI生成內容，除非我十分確定其正確性并能說服他們。

為了端到端的科學實驗，我讓Aristotle來做形式化，而不是自己動手，因為我們的目標是看AI能否獨立解決公開問題。我在推特上也因數學評測積累了一些聲望，最終通過EpochAI的聯系人獲得了GPT-5.2 Pro的使用權限。

我記得最終是利亞姆用GPT-5.2試了第 333 號問題，并讓我看看它的解法。我整體覺得是對的，于是把證明傳給我這邊的GPT-5.2 Pro轉成 TeX 輸出，再交給 Aristotle 形式化。圣誕節當天，我把這個證明發到了網站上。那一刻，首個AI原創解法的激動沖昏了我的頭腦，我判斷失誤，提前在推特上宣布了這一消息。這大概是我學術生涯至今最尷尬的時刻之一。不過當Koishi Chan發現該問題早已被文獻報道后，我迅速撤回了聲明。

為了挽回因此受損的聲望，我繼續尋找另一個問題，這次格外謹慎。過程中有幾個問題，要么是我、要么是ChatGPT發現了問題本身或已有文獻的相關情況，我都在網站上做了說明。

又是利亞姆運氣好，發現用他的工作賬號運行 GPT-5.2 Pro 可以解出第 728 號問題。他把證明發給我，我覺得合理，而且相當巧妙，巧妙運用了切爾諾夫（Chernoff）界。我把證明傳給我這邊的 GPT-5.2 Pro 檢查并整理成 TeX。

我把 TeX 交給 Aristotle，最終得到輸出結果并發到網站上。這時有人指出，問題中的 C 應取任意大，而我自己讀錯了題目，把 C 和 ? 都理解為充分小。不過我以及后來的陶哲軒都注意到，GPT-5.2的證明在舍棄k!項時有些浪費。我和利亞姆分別詢問各自的ChatGPT實例能否修正證明，他的實例先完成，模型自己也發現了我和陶哲軒注意到的問題，并輕松修正了證明。

他把修正后的證明發給我，證明策略至少看起來是可行的。（盡管有個引理的證明里，k本應對數增長卻被固定，我覺得有點可疑，但我認為這是可以修正的，只是不確定是否需要用到素數定理，那會更麻煩。）

無論如何，Aristotle最終給出了一個初等證明，形式化了GPT-5.2 Pro的證明，并通過簡單、有效且優美的顯式選擇修正了我存疑的地方。我把這個結果發到網站上，耐心等待文獻核查等。我自己之前已經查過第 728 號問題是否被解決過，盡我所能沒有找到任何記錄，因此更有信心這很可能是原創成果。

有人指出這個證明策略受到波默蘭斯（Pomerance）早期工作的啟發，似乎降低了證明的原創性。但話說回來，我認為目前這些系統還不具備提出全新思想的能力，只能組合已有思想得到新結果，所以我并不意外。

我們發現第 729 號和第 401 號問題與第 728 號非常相似，我覺得證明方法很可能可以遷移。于是我把第 728 號的證明和第 729 號的問題描述一起交給 GPT-5.2 Pro，問它能否遷移解法。果然，它給出了正確證明，后來第 401 號也同樣解決。兩個問題最終都由 Aristotle 完成形式化。（這時我發現，把第 728 號的 Lean 文件作為額外上下文傳給它，以為它能直接復用相關引理，結果反而讓 Aristotle 困惑，沒有起到幫助作用。）

利亞姆還用 GPT-5.2 Thinking 解出了第 205 號問題，Aristotle也形式化了它的解法。該解法似乎受到對應帖子里沃伊特（Woett）啟發式思路的影響。

后續影響與人工智能在數學領域的未來

在成功解決這四個問題后，很多人也開始嘗試同樣的做法。我對此表示支持，但強烈建議嘗試者具備足夠高深的數學背景，能夠理解證明并判斷其有效性。

到目前為止，這些模型已經證明自己能夠進行文獻檢索，并組合訓練數據中見過的思想來建立新結果。我們還沒看到能提出全新、有用工具與理論的模型，而這很可能是解決更難問題所必需的。

我認為先解決這些 “低垂的果實” 是件好事，能讓數學家把時間更好地用在真正值得關注的難題上。我把這次研究當作科學實驗，看模型究竟進步到了什么程度、現在能解決哪些問題。

顯然，未來的模型能力會更強。但我希望數學這項事業依然能由人類享受，而不是將來一遇到難題就丟給 GPT-8 之類的模型。我相信人類數學家永遠會扮演一個角色：理解并闡釋這些更高級模型生成的證明。但問題是，當AI模型也能做這些事時，如何為這項工作爭取足夠的資金支持？至少，我認為這將是全社會層面的問題，不只局限于數學家，因此很可能需要類似全民基本收入（UBI）的制度來適應這種變化。

在我看來，當前范式模型的極限是：能夠解決任何可以通過巧妙組合現有技術與工具來攻克的問題。這當然足以解決一些更難的問題，但我認為不足以解決最難的那些問題，比如黎曼假設。要解決這類問題，模型可能需要發展出有用的、與數論相關的?幾何定義，或是進一步探索非交換代數、登寧格（Deninger）上同調等。

對數學家而言，我認為這項技術將朝以下方向發展：

1. 更強的智能體能力，能夠大規模進行文獻檢索。大語言模型本身也會相當擅長非形式化證明到形式化證明的轉換。不過由于訓練數據中包含過時的 Lean 3 代碼，它們在處理 Lean 時會混淆，產生不存在或過時的證明策略幻覺。因此我認為，像 Aristotle 這樣專門的 Lean 自動形式化工具始終是更好的選擇。

2. 在類似 AlphaEvolve 的環境中，將擅長非形式化的大語言模型與擅長形式化的自動形式化系統結合，兩者可以來回 “交流”，這將有效減少證明生成中的幻覺問題。但要讓這一模式適配當前的研究數學，Mathlib 中需要形式化的高階成果數量還非常多。不過 AlphaGeometry 2 能在幾秒內解決奧林匹克難度的歐氏幾何問題，它的成功正是因為結合了能提出創造性構造的非形式化大語言模型與能從構造出發完成證明的符號推理器。這一思路可以抽象到更高層面，比如讓 Gemini Deep Think 與 AlphaProof 配合使用。

3. Transformer架構不容易擴展并行思路生成。我認為，如果模型要嘗試提出原創工具，并出現類似 “第37步棋” 那樣的時刻（指 AlphaGo 在與李世石第二局中那步極具創造性的棋），就需要在思維鏈的每一步進行某種并行思路生成，并執行蒙特卡洛樹搜索。要在超越人類對給定問題思考的新奇性尺度上做到這一點，可能需要更具擴展性的架構，比如擴散模型（已知它能在隱空間探索更豐富的圖景）。

   當然，由于缺乏上下文感知，擴散模型在語言建模上效果并不特別好，因此用基于 Transformer 的結果驗證模型（PRM）之類的自回歸模型引導搜索會很有用。據我所知，目前的 GPT-5.2 Pro、Gemini Deep Think、Grok Heavy 等模型，都擁有多個互相通信的基礎模型并行實例，但在思維鏈的每一步并沒有并行思路生成。這似乎是更值得探索的方向，但在 Transformer 上實現成本極高。

我10月份第一節課上，馬爾可夫鏈課程的老師開頭說過一句有意思的話：“大語言模型不過是裝了花里胡哨功能的馬爾可夫鏈；它們不是人工智能，不會推理，也沒有原創能力。” 我相信我們現在正開始看到，這句話越來越站不住腳。

讀者評論（觀點僅供參考）

親愛的凱文：感謝你分享這么精彩的故事，我非常喜歡。針對你最后一段，我有一個看法：人們仍然把 ChatGPT-5.2 這類程序稱為大語言模型（LLMs），但它們其實已經不止于此。或許叫 LLM+ 會更合適。

我也問了 Gemini 3 Pro 對這篇博客的看法，以下是回答節選：這是一篇具有歷史意義的博客文章。它精準記錄了 2025—2026 年冬天，“提示工程” 演變為 “證明工程” 的時刻。它的重點不在于數學本身，而在于用不完美的AI工具得到完美形式化證明的方法論…… 這篇故事準確指出，數學的近期未來不是AI取代數學家，而是數學家成為AI智能體的 “管理者”。

——old-bielefelder 2026年1月26日 11:44

我不太清楚 “LLM+” 指什么。我想你可能是指 LLM 加上支撐框架（比如智能體循環）。如果是這樣，GPT-5.2 Instant/Thinking 確實是 LLM（基于 Transformer 的模型）。GPT-5.2 Pro 很可能是 LLM+，在某些場景下用更復雜的框架增強 LLM，取得更好效果。

但我不確定這個區別是否很重要？如果我理解有誤，歡迎進一步解釋。

——natso26 2026年1月26日 13:08

“+” 沒有明確定義。我主要指 Python 沙盒與聯網搜索功能。

——old-bielefelder 2026年1月26日 13:55

明白了，你是指工具使用。這很合理，大致和 “框架” 是一個意思。沒錯，從這個意義上說，ChatGPT 具備工具使用能力，因此是LLM+。這里 “GPT-5.2 Thinking” 有兩層含義，可以指模型本身（LLM），也可以指用戶體驗（LLM+）。

——natso26 2026年1月26日 13:58

謝謝！我想評論幾點，或許對其他人也有用、也感興趣：

1. 關于初等數論

   我認為 “數百年的訓練數據” 對大語言模型在初等數論上的能力影響不大。畢竟現代數學大部分都依賴相當近代的工具。

   而且，即便初等數論（在某些情況下）容易用計算機驗證，我也不認為這對實際強化學習有多大影響，模型在強化學習中主要學習非形式化推理以得到答案或證明。

2. 關于 “AI 垃圾” （AI slop）一詞我建議我們避免使用帶有負面含義的詞匯，因為很明顯，在不同情況下，部分 AI 輸出可能有用且 / 或質量很高。

3. 關于聲望

   對我們這個網站的人（包括布魯姆、陶哲軒等關鍵人物）來說，你沒有損失任何聲望，我們非常看重你和你的工作。或許你可以少在意社交媒體上的言論。

4. 關于第 728 號問題的證明策略

   從后續進展以及與卡爾?波默蘭斯本人的直接通信來看，有些事情已經更清晰。

   首先，與波默蘭斯工作的相似性，似乎并沒有降低原創性。我最恰當的表述是：該方法本身從一開始就不算非常新穎。除波默蘭斯外，它也與埃爾德什的 Aufgabe 557 相似。波默蘭斯也寫過一篇筆記，把他的工作推廣到新結果，與AI的工作高度重疊，而那篇筆記本身也不算特別新穎。簡而言之，這里存在一種 “自然” 的策略，無論是埃爾德什、波默蘭斯還是 GPT-5.2 Pro，推導出來都非常相似。從整體來看，這種策略本身不算特別新穎。

   對于 “組合已有思想得到新結果”，我會非常謹慎。因為在某種層面上，整個數學都是這樣的組合；區別在于組合的難度，而不在于是否是組合。在這個框架下評價，這里的難度水平是否低于我們認為可發表的數學水平，也并不明確。

5. 關于低垂的果實

   雖然目前AI自主解決的問題在埃爾德什問題網站上屬于較容易的一類，但我認為不能說我們攻克它們是 “為了讓數學家把時間更好地用在真正值得關注的難題上”。

   顯然，這些AI成果中有一些本身就很有趣，值得關注。

6. 關于社會變革

   我提醒不要具體斷定全民基本收入（UBI）之類的影響，不確定性實在太大。

7. 關于當前范式

   我認為，把當前模型的局限等同于當前范式的局限是不正確的。

   我認為，聲稱 “像 Aristotle 這樣專門的 Lean 自動形式化工具始終是更好的選擇” 是沒有根據的。

   我認為對并行思路生成的描述存在重大不準確：第一，并行解碼確實可行，已有論文實現；第二，我不確定類似第37步棋那樣的突破為何需要并行；第三，基于擴散的大語言模型在這方面是否會優于自回歸模型，還不確定；第四，人類思維是否具有獨特的 “新奇性”，并不明確，實際上可能性很低；第五，擴散模型對語言建模是否無效，目前還沒有定論，可參考 Gemini Diffusion；第六，GPT-5.2 Pro/Gemini DeepThink/Grok Heavy 等模型很可能確實使用了并行解碼。這確實成本高昂，因此API費用昂貴。

8. 關于馬爾可夫鏈

   對于基礎大語言模型（即僅用自回歸目標訓練來擬合數據分布的模型），這句話可能有些道理。但必須注意：在本文語境下，我不確定基礎大語言模型是否 “智能”、能否 “推理”、是否具備 “原創能力”。如果非要回答，我對這三點都暫時持肯定態度。但對于推理模型，由于追求的目標不同，這句話很可能并不適用于其本意。

——natso26 2026年1月26日 13:55

參考資料

https://www.erdosproblems.com/728

https://www.erdosproblems.com/forum/thread/blog:2

https://pellaml.github.io/iumb/

https://kb799.user.srcf.net/about/

https://www.erdosproblems.com/forum/user/KStar

https://www.varsity.co.uk/science/31116

小樂數學科普本月文章

版權聲明：本文首發于微信公眾號“zzllrr小樂”的專欄《小樂數學科普》。歡迎個人轉發。如需轉載，請在“zzllrr小樂”公眾號后臺回復“轉載”，還可通過公眾號菜單、發送郵件到zzllrr@gmail.com與我們取得聯系。相關圖文音視頻內容默認遵守CC BY-NC 4.0知識共享協議，未獲作者和譯者授權，禁止用于營銷宣傳和商業目的。

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數學

更加

易學易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評論、點贊、在看、在聽

收藏、分享、轉載、投稿

查看原始文章出處

點擊底部一起捐

助力騰訊公益

點擊zzllrr小樂

公眾號主頁

右上角

置頂★加星

數學科普不迷路！