陶哲轩18个月的数学挑战，被这个“AI高斯”三周KO：人类，你还敢不敢卷？

TL;DR：

顶级数学家陶哲轩耗时18个月都没搞定的数学难题，竟然被一个名叫Gauss的AI Agent，用短短三周时间光速解决了！这波操作直接让AI在数学形式化领域“杀疯了”，也引发了我们对“人机协作”未来模式的深度思考。

“人类高质量打工人”陶哲轩最近可能有点“凡尔赛”的烦恼了。这位菲尔兹奖得主、数学界的天花板，在2024年1月和Alex Kontorovich共同提出了一个数学挑战——用Lean语言形式化强素数定理（PNT）。他们吭哧吭哧搞了18个月，直到今年7月才取得“阶段性进展”。结果呢？半路杀出个“程咬金”——一个名叫Gauss的AI Agent，只用了三周，就直接给“KO”了！

这简直是把“效率”二字刻进了DNA，让人不禁想问：这AI高斯，是不是有点太不讲武德了？

那么问题来了，这AI高斯到底是个什么来头？它背后是一家叫做Math的AI公司。据介绍，Gauss是他们家的“扛把子”，号称首个能辅助顶级数学家进行“形式验证”的自动形式化（autoformalization）Agent。说白了，它就是个超级严谨的“数学翻译官”加“验证大师”。

简单点解释，“形式化”这事儿，就是把我们人类写出来的数学公式、定理，翻译成一种机器能读懂、能检查，而且严丝合缝、没有半点歧义的“机器语言”（比如Lean）。这样做的好处就是，可以利用计算机的强大算力，逐字逐句、逐个逻辑点地检查数学证明的正确性，避免任何人类可能存在的疏漏。陶哲轩他们之所以进展缓慢，就卡在了“复分析”这个核心难题上，这玩意儿，对人类来说可真是个“老大难”。

但Gauss同学，作为硅基生命体，它可没这烦恼。它能24小时不间断地“卷”，极大地压缩了人类顶尖专家才能完成的工作量。更骚的是，Gauss还“顺手”把复分析里那些关键的缺失结果也给形式化了。这下你明白了吧？三周VS十八个月，这速度差，简直是坐上了火箭和开了拖拉机。

技术大揭秘：这AI高斯，到底开了什么挂？

虽然Math公司官方还没发布详细的技术报告，但从最终成果来看，Gauss直接生成了大约25000行Lean代码，里面包含上千个定理和定义。25000行代码，听起来不多？别被骗了！这种规模的形式化证明，以前往往需要好几年才能完成。想当年，历史上最大的单个形式化项目，可能需要十年跨度，代码量也不过是Gauss这次证明的十倍左右（最多50万行）。

再来个对比：Lean的官方数学库Mathlib，包含了大约200万行代码和35万个定理，这可是由全球600多位贡献者，花了足足八年时间才一点点搭建起来的。Gauss这次，直接把一个大型项目的体量，压缩到了三周，这速度，简直让同行看了都想“跪”！

为了让Gauss这尊“大佛”能顺畅运行，Math团队还和Morph Labs合作开发了Trinity环境基础设施。想想看，要让几千个并发的AI Agent同时工作，每个都有自己的Lean运行环境，那得多烧内存？TB级别的集群内存消耗，这背后是极其复杂的系统工程挑战。

Math团队还放出了“狠话”：

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

好家伙，这是要直接“卷”到“超级智能”和“机器数学家”的节奏啊！

数学天花板“凡尔赛”：AI再牛，人类的“数学嗅觉”才是王道？

就在大家惊叹Gauss“神仙操作”的时候，当事人陶哲轩本人也出来发表了一番“清醒发言”。他可没直接说AI“偷跑”，而是深刻剖析了人类和AI在解决复杂项目时的不同目标。

他指出，任何复杂项目都有明确目标（比如获得某个数学命题的形式化证明）和隐含目标（比如学习工具、建立社区、发现更精细的结构、培养新手）。过去，人类在完成明确目标时，这些隐含目标往往“顺带”也就实现了。但AI这波操作就有点“不按套路出牌”了：

“这些工具可以被指示去解决一个明确的目标，而不必实现如果由人类团队执行任务时可能同时实现的所有隐含目标。事实上，AI优化算法的性质决定了它们甚至可能以牺牲所有隐含目标为代价，在明确目标上取得高绩效。（参见古德哈特定律：‘当一个衡量标准成为目标时，它就不再是一个好的衡量标准。’）”²

言下之意，AI就像个“考试机器”，能高效拿到高分，但可能没体会到学习过程中的乐趣和深度。陶哲轩强调，随着AI工具越来越强大，项目组织者现在需要更努力地明确阐述所有目标，包括那些看似“不言自明”的隐含目标，才能更好地与AI协作，避免“鸡同鸭讲”。

他还提到，AI在围棋和国际象棋上虽然发展出了对局势的“嗅觉”，但在数学领域，人类特有的那种“数学嗅觉”（对代码“异味”的直觉，对正确路径的预感）是AI目前难以复制的。³ 不可否认，AI正在重塑人类科学范式，未来将成为人类探索数学和物理终极问题的重要伙伴，但无法完全取代人类的直觉和创造力。² 不过，陶哲轩也乐观预测，到2026年，我们将看到AI和数学合作，产出研究级别的数学成果。³

这才不是“小作坊”！创始人背景硬核，未来要“杀疯”？

别以为Math公司是哪个刚成立的“野路子”，他们老板Christian Szegedy可是有“实力”在身上的。他正是拿下今年AI顶会ICML时间检验奖论文的作者之一！他与Sergey Loffe在2015年提出的Batch Normalization（批次归一化，简称BatchNorm）⁴，论文引用量超过6万次，是深度学习发展史上的一个里程碑！

可以说，没有BatchNorm，深度学习可能还在小规模实验阶段摸爬滚打，是它让深度学习真正走向了大规模实用化和可靠性。这样的“AI大佬”坐镇，难怪Math公司敢放出如此豪言壮语。

Gauss的横空出世，无疑给整个数学界和AI领域都投下了一颗“深水炸弹”。它不仅证明了AI在形式化数学证明上的强大潜力，更引发了我们对未来人机协作模式的深思。AI是我们的“外挂”，还是最终的“替代者”？它能帮我们解决更多难题，但同时，我们又该如何定义和保留人类独特的价值？

目前，Math公司还没有公开Gauss的技术报告，看来我们只能“蹲”一波了。但可以肯定的是，这场由AI高斯掀起的数学革命，才刚刚开始！

引用

• AI高斯
• 陶哲轩
• 数学形式化
• Lean
• 自动形式化
• Batch Normalization