不得了，这个名叫Gauss（高斯）的新AI Agent，有点杀疯了的感觉。 这里的形式化（formalization），指的是把人类写的数学内容转换成一种机器可读、可检查、严密无歧义的形式语言，然后利用计算机帮助验证其正确 性。 而陶哲轩和Alex Kontorovich之所以目前仅取得阶段性进展，问题就卡在了复分析（complex analysis）的核心难题上。 而这个Gauss作为硅基生命，它的特点就是可以不停的工作，极大地压缩了以前只有顶尖形式化专家才能完成的工作量；与此同时，Gauss还形式化了上面 提到的复分析中关键的缺失结果。 这就是为什么它能三周解决陶哲轩18个月都未能完成的数学挑战的原因了。 因为它只用了三周的时间，就完成了陶哲轩和Alex Kontorovich提出的数学挑战—— 在Lean中形式化强素数定理（Prime Number Theorem，PNT）。 要知道，陶哲轩和Kontorovich在2024年1月提出这个挑战后，足足花了18个月（今年7月）的时间，也才取得阶段性的进展。 那么这个Gauss到底是什么来头？ 它的背后是一家叫做Math的AI公司，据介绍，Gauss是首个可 ...