AI Agent Gauss在短短三周内形式化了陶哲轩和Alex Kontorovich提出的强素数定理，远超人类数学家18个月的进展。Gauss由AI公司Math开发，是首个能协助顶级数学家进行形式验证的自动形式化Agent。它能将数学内容转化为机器可读的语言，并利用计算机验证其正确性。Gauss的快速进展得益于其持续工作能力和在复杂数学领域（如复分析）的突破。该AI生成了约25000行Lean代码，包含上千个定理和定义，这一规模以往需要多年完成。Math公司表示，Gauss将大幅缩短大型数学项目所需时间，并计划在未来一年内将形式化代码总量提升100到1000倍，致力于实现“可验证的超级智能”和“通才型机器数学家”。创始人Christian Szegedy曾是Batch Normalization的作者之一，该技术是深度学习发展的里程碑。

🚀 AI Agent Gauss在三周内完成了陶哲轩和Alex Kontorovich提出的数学挑战，将强素数定理在Lean中形式化。这一成就远超了人类数学家在18个月内取得的阶段性进展，展示了AI在复杂数学形式化方面的巨大潜力。

💡 Gauss由AI公司Math开发，其核心能力在于“自动形式化”，即将人类数学表述转化为机器可读、可验证的严密语言。这克服了传统形式化过程中的耗时和技术门槛，尤其在复分析等核心难题上取得了突破，是其快速解决挑战的关键。

⚙️ Gauss的成功得益于其强大的计算能力和持续工作模式，生成了约25000行Lean代码，包含上千个定理和定义，这一规模通常需要多年才能完成。Math公司预测Gauss将大幅缩短大型数学项目周期，并计划未来一年内将形式化代码总量提升100到1000倍，推动数学研究进入新范式。

🧠 陶哲轩的观点强调，AI工具可能只专注于明确目标，而忽略人类在协作中自然实现的隐含目标（如培养人才、社区建设等）。因此，项目组织者需要更清晰地阐述所有目标，以确保AI与人类在数学研究中的协同作用。

🌟 Math公司的创始人Christian Szegedy是Batch Normalization（BatchNorm）的共同作者，该技术是深度学习发展的关键里程碑，极大地推动了深度神经网络的训练和应用，为Gauss的研发奠定了坚实的技术背景。

不得了，这个名叫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工具测试此类项目的外部各方，则应提前与组织者协调，以防他们遗漏了一个或多个其工具不会优化的关键隐含目标。

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

值得一提的是，Math这家公司的老板也是有点实力在身上的。

因为他正是拿下今年AI定会ICML时间检验奖论文的作者之一，Christian Szegedy。

这篇论文是他和另一位作者Sergey Loffe在2015年提出的Batch Normalization（批次归一化，简称BatchNorm）。

如今，这篇论文的引用量超过6万次，是深度学习发展史上一个里程碑式的突破，极大地推动了深层神经网络的训练和应用。

可以说它是让深度学习从小规模实验，走向大规模实用化和可靠性的关键技术之一。

当然，网友们看罢Gauss之后虽然惊呼Amazing，但同时也在喊官方赶紧把论文公开喽。

至于更细节的技术内容，我们可以蹲一波了~

参考链接：[1]https://x.com/mathematics_inc/status/1966194751847461309[2]https://www.math.inc/gauss[3]https://www.math.inc/vision

欢迎在评论区留下你的想法！

金磊 发自 凹非寺量子位 | 公众号 QbitAI

本文来自微信公众号 “量子位”（ID：QbitAI），作者：关注前沿科技，36氪经授权发布。