AI给菲尔兹奖得主“改作文”？两周狂飙20万行代码，数学界直呼：这波真没法防！

TL;DR：

AI Agent “Gauss”仅用两周就暴力形式化了菲尔兹奖级别的球体堆积证明，顺手还帮数学女神改了几个Bug。数学家们感叹：以前觉得AI写诗是玩票，现在它直接来拆我们逻辑的台了！

2026年的数学界，可能要从“烧脑时代”直接快进到“烧服务器时代”了。

最近，一个名为 Gauss（硅基高斯）的AI智能体在数学圈投下了一枚核弹：它不仅独立完成了2022年菲尔兹奖得主 Maryna Viazovska 关于8维和24维“最密球体堆积问题”的形式化验证，还顺带完成了从自然语言到 20万行 Lean 代码的惊人跨越。更离谱的是，这哥们儿在“啃”论文的过程中，还给大佬发了“纠错邮件”，指出了原论文中的逻辑瑕疵。

网友锐评：这哪是辅助工具啊，这分明是直接拿着量子计算机去怼人家的算盘，人类精英在AI卷王面前，真的快要“寄”了。

“硅基高斯”下凡：5天干完人类15个月的活

先科普一下这个让数学家秃头的“球体堆积问题”。简单来说，就是在一堆橙子中间怎么摆最省空间。三维空间大家都懂，但到了8维和24维，那种复杂程度就像是在玩一种超越人类感官的超级魔方。Viazovska 女神当年凭借证明这俩维度的最密堆积方案，直接封神摘得菲尔兹奖。¹

然而，数学家的论文通常是自然语言写的。虽然逻辑严密，但在电脑看来，这些充满了“理应如此”、“显而易见”的文字简直就是“逻辑黑洞”。要把这些论文变成计算机能100%验证的 Lean 形式化代码，难度不亚于把《红楼梦》翻译成能在服务器上跑的C++程序。

在此之前，人类专家团队折腾了15个月才堪堪搭了个架子。结果 Gauss 进场后，画风突变：5天搞定8维证明，一周搞定更复杂的24维证明。² 这种效率，让还在实验室抠脑壳的数学家们直呼：救命，AI已经卷疯了！

离谱：它不仅会证，还会给大佬“找茬”

Gauss 的强悍之处不仅在于“快”，更在于它那比处女座还严谨的纠错直觉。

在形式化 Lean 代码的过程中，社区通常会把暂时证明不出来的步骤标注为 “sorry”。对人类来说，填补这些“坑”需要翻烂几十篇文献。但 Gauss 却展现出了惊人的“自主重构”能力：

1. 主动搜寻：它通过检索模块狂扫了几十年的关联论文，自己给自己补课。³
2. 硬刚瑕疵：在处理原论文第14页的一个不等式推导时，Gauss 连续推理了4096步，最后给出了编译错误提示。原来，强如菲尔兹奖得主，在论文里也有一处排版错误和微观逻辑瑕疵。
3. 自主修补：在没有任何人类干预的情况下，它自己重构了边界条件，把这段缺失的证明给补上了。²

这就好比你让 AI 帮你写论文，结果它写完之后告诉你：“主人，你参考的那本教材第58页印错了，我已经帮你改过来了。”这种反客为主的智力压制，确实让人有点脊背发凉。

范式转移：数学正从“文学”变成“软件工程”

Gauss 背后的公司 Math Inc. 创始人 Christian Szegedy（这位也是 xAI 的联合创始人，BatchNorm 的作者）认为，我们正在经历一场数学界的工业革命。¹

长期以来，数学证明就像是写小说，全靠同行评审的眼力劲。但现在，数学正从“自然语言文学”转向“可运行的软件工程”。这就像是从手动打孔纸带时代进入了高级语言时代。

“这种技术的最终结果将是解放数学家……让他们去梦想新的数学世界。”³

未来的数学家可能不再需要花几年的时间去验证一个公式的对错，而是作为“架构师”去设计证明思路，剩下的繁琐推理和逻辑搬砖，统统交给像 Gauss 这样的推理智能体。

当真理的验证权逐渐从人类大脑移交给服务器中那 202200 行比特流时，我们不得不思考：在那个超越人类直觉的未知疆域，AI 还会带给我们多少惊喜（或者惊吓）？

引用

• AI Gauss
• 菲尔兹奖
• Lean形式化
• 数学工程化
• 逻辑纠错