高斯AI三周破解数学难题，震撼数学界

令人惊叹的是，名为Gauss（高斯）的新AI Agent，展现出了惊人的能力。

它仅仅用了三周的时间，就完成了由陶哲轩和Alex Kontorovich提出的数学挑战——在Lean中形式化强素数定理（Prime Number Theorem，PNT）。

要知道，陶哲轩和Kontorovich在2024年1月提出这个挑战后，经过18个月的努力（直至今年7月），才取得阶段性成果。

那么，这个Gauss究竟是何方神圣？

原来，它背后是名为Math的AI公司。据介绍，Gauss是首个能协助顶级数学家进行形式验证的自动形式化（autoformalization）Agent。

所谓形式化（formalization），就是将人类撰写的数学内容转换为一种机器可读、可验证、无歧义的形式语言，再利用计算机进行验证。

陶哲轩和Alex Kontorovich之所以进展缓慢，是因为卡在了复分析的核心难题上。而Gauss作为硅基生命，其特点在于可以持续工作，极大地缩减了以前只有顶尖形式化专家才能完成的工作量，并形式化了复分析中的关键缺失结果。

这就是它能在三周解决陶哲轩耗时18个月都未能完成的数学挑战的原因。

Gauss如何实现？

目前Math公司官方尚未发布具体技术报告。

但从结果来看，Gauss生成了约25000行Lean代码，包含上千个定理和定义。这种规模的形式化证明，以前往往需要多年才能完成。

历史上最大的单个形式化项目（通常需要数年时间），也只是比这大一个数量级（最多50万行代码）。相比之下，Lean的标准数学库Mathlib有约200万行代码，包含35万个定理，由600多位贡献者耗时8年建立。

为了支撑Gauss运行，团队与Morph Labs合作开发了Trinity环境基础设施。因为要让Gauss如此大规模运行，涉及数千个并发Agent，每个Agent都有自己的Lean运行环境，会消耗数TB的集群内存，是一个复杂的系统工程挑战。

Math团队还表示：

Gauss将大幅缩短完成大型数学项目所需的时间。随着算法不断进步，我们计划在未来12个月内，让形式化代码的总量提升100到1000倍。这将成为新范式的训练场——走向“可验证的超级智能”和“通才型机器数学家”。

创始人背景不凡

值得一提的是，Math公司的老板实力非凡。

他正是获得今年AI盛会ICML时间检验奖论文的作者之一——Christian Szegedy。

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

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

可以说，它让深度学习从小规模实验走向大规模实用化和可靠性。

网友们对Gauss的表现既惊叹又期待官方公开更多细节和技术内容。至于更具体的技术内容，我们可以拭目以待了~