陶哲轩18个月没搞定的数学挑战，被这个“AI高斯”三周完成了

量子位·2025年09月14日 13:14

创始人是ICML'25时间检验奖作者

不得了，这个名叫Gauss（高斯）的新AI Agent，有点杀疯了的感觉。

因为它只用了三周的时间，就完成了陶哲轩和Alex Kontorovich提出的数学挑战——

在Lean中形式化强素数定理（Prime Number Theorem，PNT）。

要知道，陶哲轩和Kontorovich在2024年1月提出这个挑战后，足足花了18个月（今年7月）的时间，也才取得阶段性的进展。

那么这个Gauss到底是什么来头？

它的背后是一家叫做Math的AI公司，据介绍，Gauss是首个可以协助顶级数学家进行形式验证的自动形式化（autoformalization）Agent：

这里的形式化（formalization），指的是把人类写的数学内容转换成一种机器可读、可检查、严密无歧义的形式语言，然后利用计算机帮助验证其正确性。

而陶哲轩和Alex Kontorovich之所以目前仅取得阶段性进展，问题就卡在了复分析（complex analysis）的核心难题上。

而这个Gauss作为硅基生命，它的特点就是可以不停的工作，极大地压缩了以前只有顶尖形式化专家才能完成的工作量；与此同时，Gauss还形式化了上面提到的复分析中关键的缺失结果。

这就是为什么它能三周解决陶哲轩18个月都未能完成的数学挑战的原因了。

Gauss是如何实现的？

目前Math公司官方并没有发布具体的技术报告。

但从最终结果来看，Gauss生成了大约25000行Lean代码，包含上千个定理和定义。

要知道，这种规模的形式化证明，以前往往需要多年才能完成。

历史上最大的单个形式化项目（往往需要跨甚至10年的时间），也只是比这大一个数量级（最多50万行代码）。

相比之下，Lean的标准数学库Mathlib有约200万行代码，包含35万个定理，但却由600多位贡献者花了8年时间才建立起来。

为了支撑Gauss的运行，团队还和Morph Labs合作开发了Trinity环境基础设施。

因为要让Gauss如此大规模运行，会涉及数千个并发Agent，且每个Agent都有自己的Lean运行环境，会消耗数TB的集群内存，是一个极其复杂的系统工程挑战。

Math团队还表示：

Gauss将大幅缩短完成大型数学项目所需的时间。

随着算法不断进步，我们计划在未来12个月内，让形式化代码的总量提升100到1000倍。

这将成为新范式的训练场——走向“可验证的超级智能”和“通才型机器数学家”。

而就在刚刚，陶哲轩本人在Mastodon上对形式化相关的问题做了一番解释（以下为陶哲轩的陈述）。

任何复杂的项目往往都有明确陈述的目标和隐含的未陈述目标。例如，一个Lean形式化项目的明确目标可能是获得某个数学命题X的形式化证明；但通常还有一些未陈述的目标，例如以适合上游到 Mathlib 库的方式形式化X的关键子命题和定义X1, X2, …；学习如何使用各种协作工具和分配任务；有机地发现X证明的更精细结构，这在以前的非形式化证明中可能没有被强调；为新手形式化者提供实际培训和经验；以及更普遍地建立一个精通形式化艺术的人类社区。

过去，通常没有必要阐明这些隐含目标，因为这些目标的实现与明确目标的实现之间存在很强的经验相关性。在形式化项目的例子中，几乎任何以人为中心的努力来实现明确目标，最终都会自然而然地实现上述大部分隐含目标。因此，明确目标有效地成为了更广泛实际目标的可行替代。

然而，随着功能强大的AI工具的出现，情况正在发生变化，这些工具采用与人类截然不同的方法。这些工具可以被指示去解决一个明确的目标，而不必实现如果由人类团队执行任务时可能同时实现的所有隐含目标。事实上，AI优化算法的性质决定了它们甚至可能以牺牲所有隐含目标为代价，在明确目标上取得高绩效。（参见古德哈特定律：“当一个衡量标准成为目标时，它就不再是一个好的衡量标准。”）

鉴于这些工具的日益部署，这向我表明，项目组织者现在需要付出更大的努力，明确阐述项目的所有目标，而不仅仅是名义上的目标。在某些情况下，这些目标甚至可能最初对组织者自己来说并不明显，可能需要参与者之间进行一些讨论。而有兴趣用其AI工具测试此类项目的外部各方，则应提前与组织者协调，以防他们遗漏了一个或多个其工具不会优化的关键隐含目标。