当AI以可验证的方式攻克数学难题——它如何重写了科研的成本与门槛2025年12月一个AI系统用6小时独立完成了一道困扰数学界30年的难题的证明并用证明助手在1分钟内完成了形式化验证。这不是孤例而是一条加速曲线上的最新节点。当AI的数学发现从看起来像对的变成每一步都被机器验证过它改变的不仅仅是数学——它重新定义了什么算做研究、谁有资格做研究、以及一项发现需要多少成本。一、一条清晰的加速曲线要理解2025年底发生的事情需要回看整条时间线。这不是某一天的突变而是一系列里程碑累积的结果。2022年10月AlphaTensor——50年矩阵乘法算法的首次改进DeepMind在《Nature》发表封面论文推出AlphaTensor。这个基于AlphaZero的系统将矩阵乘法算法的发现问题转化为一个单人博弈在4×4有限域矩阵乘法上首次改进了Strassen 1969年提出的算法——这是该问题50年来的第一次进步。更重要的是AlphaTensor为每种矩阵尺寸发现了多达数千种正确算法揭示了算法空间远比人类想象的丰富。论文地址https://www.nature.com/articles/s41586-022-05172-42023年12月FunSearch——LLM首次在开放数学问题上有新发现DeepMind在《Nature》发表论文介绍FunSearch方法。这是首次有人用大语言模型在具有挑战性的开放科学/数学问题上做出新发现。FunSearch将LLM与自动评估器配对通过演化策略迭代LLM生成候选方案以代码形式评估器自动验证并打分最优方案进入下一轮。FunSearch在**帽子集问题cap set problem**上取得了突破——这是极值组合学中的一个核心开放问题著名数学家陶哲轩曾称其为我最喜欢的开放问题。该问题困扰多个研究领域的数学家数十年暴力计算完全不可行可能性数量超过宇宙中的原子数。FunSearch发现了20年来最大的帽子集构造超越了最先进的计算求解器。研究团队与威斯康星大学麦迪逊分校的Jordan Ellenberg教授合作——他正是帽子集问题的重要突破者之一。论文地址https://www.nature.com/articles/s41586-023-06924-62024年7月AlphaProof——IMO银牌DeepMind的AlphaProof联合AlphaGeometry 2在2024年国际数学奥林匹克竞赛IMO中解出6题中的4题获得28分满分42达到银牌水平仅差1分就是金牌。这是AI首次在IMO登上领奖台。AlphaProof的核心创新在于将强化学习引入Lean形式化证明环境所有推理步骤必须符合形式化逻辑规则因此每一步推理都可以被自动验证。团队先对约8000万个数学命题进行自动形式化处理再用强化学习让系统在这些命题中探索证明路径。IMO主席Gregor Dolinar评价“AI最终将能比人类更好地解决大多数数学问题其进步速度令人惊叹。”该成果于2025年11月12日正式发表在《Nature》上。2025年5月AlphaEvolve——330年亲吻数问题的突破DeepMind发布AlphaEvolve一个由Gemini驱动的进化编码智能体。在数学领域AlphaEvolve取得了多项突破亲吻数问题——这个问题的历史可以追溯到1694年牛顿与大卫·格雷戈里在剑桥的争论在一个中心球周围最多能紧贴放置多少个相同大小的球三维空间的答案是12牛顿是对的但直到1953年才被严格证明。当维度升高问题变得极其困难。AlphaEvolve在11维空间中找到了593个球体的排列方式超越了此前592的纪录。矩阵乘法——AlphaEvolve找到了一种4×4复值矩阵乘法算法仅需48次标量乘法改进了Strassen 1969年的算法。这是56年来的首次改进。在DeepMind测试的50多个开放数学问题中AlphaEvolve在约75%的问题上重新发现了最前沿解法在约20%的问题上直接超越了已知最佳结果。AlphaEvolve的实际应用同样引人注目它发现的调度算法已在Google数据中心运行一年多平均持续回收全球0.7%的计算资源它优化了Gemini架构中的矩阵乘法核心训练时间缩短了1%。2025年12月Aristotle——6小时与30年2025年12月1日HarmonicMath公司开发的AI数学家亚里士多德Aristotle在6小时内独立完成了Erdős问题#124的证明并用Lean证明助手在1分钟内完成形式化验证。整个过程没有任何人工干预。Erdős问题#124由著名数学家保罗·埃尔德什于1995年提出涉及组合数论30年来一直悬而未决。普林斯顿大学数学博士Boris Alexeev将问题输入Aristotle后系统搜索了上亿种证明策略最终输出了100%可验证的定理。但这里必须诚实Aristotle解决的是该问题的较弱版本。原始问题有两个不同版本Aristotle解决的是较简单的那个。erdosproblems.com网站的维护者Thomas Bloom评价道事后来看解决方案相当简单使得这个问题处于数学竞赛题的水平。不过他也承认“这是一个很好的证明完全由人工智能从形式化陈述出发、无人工干预生成然后在Lean中形式化这本身已经令人印象深刻。”菲尔兹奖得主陶哲轩对此评论道当前存在大量数学问题本身相对容易证明或证伪但由于能够投入研究的人类专家数量有限这些问题长期未获关注。如果借助自动化工具进行大规模处理可以先清理那些最容易的问题把真正困难的部分留给人类数学家。2025-2026年Gauss——菲尔兹奖成果的形式化验证Math, Inc.公司开发的AI系统Gauss在形式化验证领域创造了历史2025年6月用3周时间完成了强素数定理PNT在Lean中的形式化——这项任务原本是陶哲轩和Alex Kontorovich一直在努力攻克的。8维球堆积问题用5天完成了项目团队估算需要6个月才能完成的剩余验证工作。该证明由2022年菲尔兹奖得主Maryna Viazovska完成这是21世纪首个完成形式化验证的菲尔兹奖获奖成果。24维球堆积问题仅以原始论文为输入耗时两周完成了自动形式化验证。球堆积问题形式化验证的代码总量从7万行增至约20万行。作为对比Mathlib数学库自2017年起由600余位贡献者共同搭建目前代码量约为200万行。人类团队开展的单一目标形式化验证项目往往需要研究者投入整个职业生涯耗时十余年甚至更久。二、可验证为何是关键词上述每一个成果都有一个共同特征结果可以被机器独立验证。这是AI在数学领域与其他领域如写诗、画画、编程的根本区别。当ChatGPT写一段代码你不确定它是否正确当AI画一幅画你不确定它是否准确。但当AI在Lean中完成一个证明每一步推理都经过形式化逻辑规则的自检——不存在看起来对但实际上错的可能。Lean是一种编程语言兼证明助手。在Lean中数学命题被表示为类型证明被表示为程序。如果程序能通过类型检查证明就是正确的。这种保证是绝对的、不依赖人类判断的。这就是为什么Thomas Bloom虽然认为Aristotle解决的Erdős #124只是竞赛题水平但仍然承认由于证明已经在Lean证明助手中形式化也就是说每一步推理都经过了机器验证显然它确实有效。这种可验证性消除了AI研究中最令人担忧的问题——“幻觉”。在数学中一个错误步骤会让整个证明失效而形式化验证能够精确地抓住每一个错误。这使得AI的数学发现具有其他领域无法比拟的可信度。三、成本重写从职业生涯到计算小时让我们用具体数字来感受这种成本结构的变化任务传统方式AI方式加速比Erdős #124弱化版30年未解6小时数千倍8维球堆积形式化验证剩余工作估算6个月Gauss用5天~36倍24维球堆积形式化验证从零开始数年Gauss用2周仅以论文为输入数十倍强素数定理形式化Tao等人长期未完成Gauss用3周—Erdős #1026传统方法需数周至数月人机协作48小时数倍至数十倍帽子集问题新构造20年未有进展FunSearch迭代生成—陶哲轩在回顾Erdős #1026的解决过程时说用传统方法一两位数学家用简单的编程和文献检索工具最终也能完成但可能需要数周或者数月才能解决。而在AI辅助下整个过程48小时就完成了。这里的关键不是AI比人类聪明——至少目前还不是。关键在于成本的量级变化。一个人类数学家解决一个问题需要数月到数年这背后是数十年的专业训练和积累。而AI运行一次实验消耗的是计算小时——一种可以并行、可以复制、成本持续下降的资源。当研究的瓶颈从人类智力与时间转移到算力与算法设计整个科研经济学就变了。四、门槛重写从精英俱乐部到众包AI2024年9月陶哲轩启动了方程理论项目Equational Theories Project。他考虑了一种叫做原群magma的简单数学对象提出了数千个描述原群中元素行为的命题想评估所有这些命题之间约2200万种可能的蕴含关系。这是一个个体或小团队根本无法完成的规模。但项目启动后50多名参与者——其中许多是业余爱好者——使用AI和自动证明工具协同工作。几个月内超过99%的蕴含关系被证明或证伪。项目还发现了一种此前从未被描述过的数学结构被研究者称为原群上同调magma cohomology。陶哲轩描述了他对未来的设想“未来当我们探索数学的一个领域时你可以首先让一个AI来探索数百万个问题并获得一些初步的景观。只是质量很低。但这将引导更老练的人类说‘好吧现在根据这种实验我们应该将我们的人力资源用在这里。’”他将当前的AI比作一个过度自信的本科生——不能独立解决前沿数学问题但如果采用三方协作模式AI清理大量简单子问题、人类处理困难核心部分、Lean严格验证结果就能产生惊人的效果。这种模式意味着参与前沿数学研究的门槛正在降低。你不需要是菲尔兹奖得主就能做出贡献——你需要的是会使用AI工具、理解Lean的基本概念、以及愿意投入时间。Erdős问题网站已经公开鼓励使用AI辅助解题只需满足三个条件公开说明使用了AI、内容由用户独立验证、评论长度合理。五、数学的实验科学转向陶哲轩多次将AI时代的数学研究与粒子物理学做类比。物理学曾经是少数理论家独立思考的领域如今已经变成CERN那样数百名专家分工协作的大型实验科学。他认为数学正在经历类似的转变。这种转变体现在几个层面1. 探索方式的改变。传统数学研究依赖直觉和理论洞察而AI可以进行大规模系统性搜索。AlphaEvolve在50多个开放问题上的表现以及PackingStar上海科学智能研究院、北京大学、复旦大学联合开发在亲吻数问题多维度上的连续突破都展示了这种搜索能力的威力。PackingStar在12维至31维的多个维度刷新了亲吻数纪录发现了6000余个新构型获得了MIT教授Henry Cohn的高度评价。2. 协作模式的改变。Erdős #1026的解决过程是一个典型案例多位数学家通过在线论坛协作使用AlphaEvolve生成上界、用ChatGPT Pro可视化、通过AI论文检索找到关键参考文献、最终用ChatGPT整合证明——48小时内完成了一个50年未解的问题。陶哲轩本人还用Gemini 2.5 Deep Think在十分钟内完成了Erdős #367的论证分析用GPT-5进行半自动化文献检索并发现部分Erdős问题其实早已被解决。3. 验证方式的改变。形式化验证不再只是辅助工具而是成为发现过程本身的一部分。2024年12月Renaissance Philanthropy和XTX Markets宣布启动AI for Math Fund首期920万美元资助专注于自动定理证明领域。陶哲轩担任顾问委员会成员。六、诚实的边界AI还不能做什么在为AI的能力惊叹之余必须诚实地面对它的局限。第一AI解决的可能不是最难的部分。Aristotle解决的Erdős #124是弱化版本原始问题仍然开放。Bloom指出如果简单的证明方法有效那么Burr、Erdős、Graham和Li这样的联合智慧肯定早就发现了。第二AI的速度仍然有限。AlphaProof在IMO 2024中解3道题花了3天而人类选手只有4.5小时。它也没有解决两道组合数学问题。第三AI无法提出好问题。AlphaProof和AlphaEvolve都是在人类设定的问题框架内工作。正如伦敦数学科学研究所的何杨辉所指出的这类系统对于帮助数学家证明问题很有用但无法帮助研究人员确定需要解决和研究的问题。第四AI的构造不总是有数学洞察。AlphaEvolve在11维亲吻数问题上的593球构造被研究者评价为较为混乱缺乏内在的数学结构。相比之下PackingStar通过重新定义问题获得了更有结构的构型——但PackingStar自身也无法为新构型提供数学证明需要人工验证。第五形式化验证本身有成本。MathLib数学库自2017年起由600余位贡献者搭建目前约200万行代码——而这只覆盖了数学知识的一部分。很多前沿数学还无法被直接形式化。陶哲轩的判断是审慎而乐观的AI正在高效地收割数学界的低垂果实让人类研究者得以聚焦更具挑战性的核心问题。但真正困难的数学——那些需要全新概念和深刻洞察的工作——仍然是人类的领域。七、真正的变革回到开头的问题当AI第一次以可验证的方式独立解决了困扰数学家数十年的难题它证明了能力但更重要的是——它重新定义了科研的成本与门槛。这句话的含义现在应该更清楚了能力证明——从AlphaTensor到AristotleAI已经证明它可以在多个数学分支做出超越人类已知最优的结果并且这些结果可以通过形式化验证确保绝对正确。成本重写——一项发现从需要一个数学家数年的职业生涯变成需要数小时的计算。这并不意味着数学家变得多余而是意味着同样的智力投入可以覆盖远多得多的命题空间。门槛重写——从需要数十年专业训练的精英到会使用AI工具的业余爱好者也能参与。Erdős问题网站上的变化是最直观的证据最近该网站上未解标签减少了近十个并非因为人类突然解决了这些问题而是AI通过文献检索发现它们早已被攻克——只是长期没人注意到。真正值得关注的不是任何一个单独的突破而是结构性变化当验证不再依赖人类信任、当搜索不再依赖人类直觉、当协作不再受限于地理和机构——科研的产出方式正在发生根本性转变。陶哲轩说在Erdős问题网站上“AI辅助已经变得很常见”。这句话比任何单个突破都更能说明问题。当一个工具从令人震惊的新闻变成日常工作流的一部分变革就已经发生了。数学是科学的基石。如果连数学这种对严谨性要求最高的学科都在被AI重新定义那么其他领域的科研成本与门槛被重写只是时间问题。本文所有事实均来自公开可查的来源包括Nature论文、DeepMind官方博客、中国科学院网信工作网、人民网、澎湃新闻、陶哲轩个人博客等。文中涉及的具体数字、时间、人物和成果均可追溯验证。主要参考来源Romera-Paredes et al., “Mathematical discoveries from program search with large language models,” Nature, Dec 2023Fawzi et al., “Discovering faster matrix multiplication algorithms with reinforcement learning,” Nature, Oct 2022DeepMind, “AI achieves silver-medal standard solving IMO problems,” July 2024DeepMind, “AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms,” May 2025DeepMind, “AlphaProof,” Nature, Nov 2025Bardai, “AI cracks 30-year math problem,” Dec 2025陶哲轩个人博客terrytao.wordpress.com中科院网信工作网、人民网、澎湃新闻、36氪等相关报道