#AI三周完成陶哲轩数学挑战##陶哲轩18个月未解数学题被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之所以目前仅取得阶段性进展，问题就卡在了复分析（complex analysis）的核心难题上。

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

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