陶哲轩惊呼“变天”，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将其转化为严谨证明。