陶哲轩18个月没搞定的数学挑战，被这个“AI高斯”三周完成了

Math 公司开发的 AI Agent Gauss 仅用三周时间完成陶哲轩与 Alex Kontorovich 花费 18 个月才取得阶段性成果的数学挑战——在 Lean 中形式化强素数定理。Gauss 生成约 25,000 行代码，形式化上千定理，突破复分析难题。Math 表示 Gauss 可大幅缩短大型数学项目周期，并计划一年内将形式化效率提升百至千倍。陶哲轩指出 AI 可能忽略项目隐含目标，呼吁提前协调。公司创始人之一为深度学习里程碑技术 BatchNorm 的提出者。
来源：https://mp.weixin.qq.com/s/TH-5dDu5rmTy2b2tEZLz0w