[谷歌] 震驚,谷歌AI壹夜連破9道世紀難題
以Erdős #125為例，它的解題過程是這樣的。
首先，子智能體先用思維鏈推理分析問題結構，然後通過搜索替換修改Lean代碼，接著調用AlphaProof處理子目標。
AlphaProof搞定了6個子目標中的3個，子智能體隨即將剩余的“硬骨頭”分解為更小的引理，再次調用AlphaProof——這次，全部搞定。
整個過程中，沒有任何人類數學家介入。
9道Erdős問題，56年前的懸案壹朝告破DeepMind將完整版Agent D投放到353道已形式化的Erdős問題上。每道題最多允許3000輪迭代。
最終，9道問題被攻克。
其中含金量最高的幾道：
1. Erdős #12（1970年提出）
是否存在壹個無限集A，滿足“任意叁個不同元素a
這道題懸置了56年，期間多位數學家取得了部分進展，但始終無法給出完整構造。
AI的解法精妙地結合了中國剩余定理和叁項等差數列回避集，通過構建壹系列精心設計的“區塊”來同時滿足密度條件和整除約束。
2. Erdős #125（1996年提出）
在叁進制下只用數字0和1的整數集A，加上肆進制下只用數字0和1的整數集B，它們的和集A+B的下密度是否為正？
AI證明了答案是否定的——下密度為零。
證明的核心是壹個歸納稀疏化論證，巧妙利用了3^m和4^k的丟番圖逼近性質（log4/log3是無理數），通過反復找到兩個基數幾乎對齊的尺度，讓密度以0.99的比率逐步衰減到零。
3. Erdős #138（1981年提出的變體）
van der Waerden數W(k+1) - W(k)是否趨於無窮？
AI給出了壹個極其優雅的證明：W(k+1) ≥ W(k) + k。核心思路是貪心染色擴展——在壹個沒有單色k-AP的2-著色基礎上，逐個添加新元素，用反證法說明貪心策略不會失敗。
4. Erdős #846
這是壹個關於平面點集中共線性質的問題。
而AI的構造，令人歎為觀止。
它把完全圖K∞的每條邊映射到平面上的壹個點，用贰次多項式編碼坐標，然後利用無窮Ramsey定理完成證明。
目前，所有9道問題的Lean證明代碼已開源在GitHub上。
[加西網正招聘多名全職sales 待遇優]
這條新聞還沒有人評論喔，等著您的高見呢
首先，子智能體先用思維鏈推理分析問題結構，然後通過搜索替換修改Lean代碼，接著調用AlphaProof處理子目標。
AlphaProof搞定了6個子目標中的3個，子智能體隨即將剩余的“硬骨頭”分解為更小的引理，再次調用AlphaProof——這次，全部搞定。
整個過程中，沒有任何人類數學家介入。
9道Erdős問題，56年前的懸案壹朝告破DeepMind將完整版Agent D投放到353道已形式化的Erdős問題上。每道題最多允許3000輪迭代。
最終，9道問題被攻克。
其中含金量最高的幾道：
1. Erdős #12（1970年提出）
是否存在壹個無限集A，滿足“任意叁個不同元素a
這道題懸置了56年，期間多位數學家取得了部分進展，但始終無法給出完整構造。
AI的解法精妙地結合了中國剩余定理和叁項等差數列回避集，通過構建壹系列精心設計的“區塊”來同時滿足密度條件和整除約束。
2. Erdős #125（1996年提出）
在叁進制下只用數字0和1的整數集A，加上肆進制下只用數字0和1的整數集B，它們的和集A+B的下密度是否為正？
AI證明了答案是否定的——下密度為零。
證明的核心是壹個歸納稀疏化論證，巧妙利用了3^m和4^k的丟番圖逼近性質（log4/log3是無理數），通過反復找到兩個基數幾乎對齊的尺度，讓密度以0.99的比率逐步衰減到零。
3. Erdős #138（1981年提出的變體）
van der Waerden數W(k+1) - W(k)是否趨於無窮？
AI給出了壹個極其優雅的證明：W(k+1) ≥ W(k) + k。核心思路是貪心染色擴展——在壹個沒有單色k-AP的2-著色基礎上，逐個添加新元素，用反證法說明貪心策略不會失敗。
4. Erdős #846
這是壹個關於平面點集中共線性質的問題。
而AI的構造，令人歎為觀止。
它把完全圖K∞的每條邊映射到平面上的壹個點，用贰次多項式編碼坐標，然後利用無窮Ramsey定理完成證明。
目前，所有9道問題的Lean證明代碼已開源在GitHub上。
[加西網正招聘多名全職sales 待遇優]
| 分享: |
| 注： | 在此頁閱讀全文 |
| 延伸閱讀 | 更多... |
推薦: