[谷歌] 震惊,谷歌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上。
[物价飞涨的时候 这样省钱购物很爽]
好新闻没人评论怎么行，我来说几句
首先，子智能体先用思维链推理分析问题结构，然后通过搜索替换修改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上。
[物价飞涨的时候 这样省钱购物很爽]
| 分享: |
| 注： | 在此页阅读全文 |
| 延伸阅读 | 更多... |
推荐: