“AI高斯”三周完成陶哲轩18个月未搞定的数学挑战，创始人来头不小

09-15 06:27

不得了，这个名叫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作为硅基生命，能不停工作，极大压缩了以往只有顶尖形式化专家才能完成的工作量。同时，它还形式化了复分析中关键的缺失结果。这就是它能三周解决陶哲轩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优化算法性质决定了它们可能以牺牲隐含目标为代价，在明确目标上取得高绩效。鉴于这些工具的广泛应用，项目组织者需更努力明确阐述项目所有目标，而非仅名义目标。