当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-4

2023年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-6

2024年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的数学发现具有其他领域无法比拟的可信度。

三、成本重写：从"职业生涯"到"计算小时"

让我们用具体数字来感受这种成本结构的变化：

陶哲轩在回顾Erdős #1026的解决过程时说："用传统方法，一两位数学家用简单的编程和文献检索工具，最终也能完成，但可能需要数周或者数月才能解决。"而在AI辅助下，整个过程48小时就完成了。

这里的关键不是"AI比人类聪明"——至少目前还不是。关键在于成本的量级变化。一个人类数学家解决一个问题需要数月到数年，这背后是数十年的专业训练和积累。而AI运行一次实验，消耗的是计算小时——一种可以并行、可以复制、成本持续下降的资源。

当研究的瓶颈从"人类智力与时间"转移到"算力与算法设计"，整个科研经济学就变了。

四、门槛重写：从"精英俱乐部"到"众包+AI"

2024年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到Aristotle，AI已经证明它可以在多个数学分支做出超越人类已知最优的结果，并且这些结果可以通过形式化验证确保绝对正确。

成本重写——一项发现从需要"一个数学家数年的职业生涯"变成需要"数小时的计算"。这并不意味着数学家变得多余，而是意味着同样的智力投入可以覆盖远多得多的命题空间。

门槛重写——从需要"数十年专业训练的精英"到"会使用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 2023
• Fawzi et al., “Discovering faster matrix multiplication algorithms with reinforcement learning,” Nature, Oct 2022
• DeepMind, “AI achieves silver-medal standard solving IMO problems,” July 2024
• DeepMind, “AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms,” May 2025
• DeepMind, “AlphaProof,” Nature, Nov 2025
• Bardai, “AI cracks 30-year math problem,” Dec 2025
• 陶哲轩个人博客：terrytao.wordpress.com
• 中科院网信工作网、人民网、澎湃新闻、36氪等相关报道