当硅基数学家超越人类顶尖头脑
2025年9月，一则爆炸性消息震动数学与AI界：由初创公司Math开发的AI Agent “Gauss”（高斯），仅用 三周时间 就完成了 陶哲轩（Terence Tao）和Alex Kontorovich 提出的数学挑战——在形式化证明工具 Lean 中完成 强素数定理（PNT） 的严格编码。而这项挑战，自2024年1月提出后，连陶哲轩这样的菲尔兹奖得主领衔的人类团队也花了 18个月 仅取得阶段性进展。
这一事件不仅标志着AI在数学形式化领域的突破性进展，更揭示了一种全新的科研范式：“Autoformalization”（自动形式化） 正在重塑人类对数学真理的探索方式。而背后的推手，正是曾因 Batch Normalization（批归一化） 推动深度学习革命的AI先驱 Christian Szegedy。
挑战是什么？为什么它如此困难？
1. 强素数定理（PNT）的形式化：数学界的”珠穆朗玛峰”
强素数定理（Prime Number Theorem）是数论中的核心定理之一，描述了素数分布的渐近规律。尽管其非形式化证明早已被数学家熟知（如19世纪黎曼假设的相关工作），但 在Lean中实现其严格的形式化证明 却异常艰难。
- 形式化的本质：将人类自然语言或数学符号描述的定理，转化为计算机可验证的 严密逻辑代码（如Lean的依赖类型理论）。这不仅要求证明本身正确，还需确保每一步推理都符合机器逻辑，无歧义。
- 复分析的瓶颈：陶哲轩团队卡在了 复分析（Complex Analysis） 的关键步骤上——这是数学中高度抽象的分支，涉及无穷级数、解析函数等复杂概念，对AI和人类都是巨大挑战。
2. 人类团队的局限
陶哲轩和Kontorovich带领的人类数学家花了18个月，仅能完成部分形式化工作。原因包括：
- 效率问题：人类专家需花费大量时间处理低级细节（如定义精确的数学对象），而非专注于核心证明逻辑。
- 协作复杂性：大型形式化项目需要多人协作，而沟通成本和任务分配可能拖慢进度。
- 隐含目标的缺失：如陶哲轩后来指出的，形式化不仅是”证明定理”，还包括 优化代码结构、适配数学库（Mathlib）、培养新手社区 等隐性目标——而AI可以更专注地直接冲击核心问题。
Gauss如何三周破解难题？
1. Gauss是什么？——首个”自动形式化数学家”
Gauss是Math公司开发的 AI Agent，其核心能力是 “Autoformalization”（自动形式化），即：
- 自动翻译数学语言：将人类书写的数学证明（如LaTeX或自然语言描述）转换为Lean等工具可执行的严格代码。
- 自主填补知识空白：在形式化过程中，Gauss不仅能复现已知证明，还能 自动推导缺失的中间定理（如复分析中的关键引理）。
- 超大规模并行计算：团队与Morph Labs合作开发了 Trinity基础设施，支持数千个并发Agent同时运行，消耗数TB级内存，模拟”硅基数学家军团”的高效协作。
2. 技术突破：25000行Lean代码的诞生
- 代码规模：Gauss最终生成了 约25000行Lean代码，包含 上千个定理和定义——相当于人类团队数年的工作量。
- 历史对比：
- Lean的数学库 Mathlib 耗时8年、由600多位贡献者建成，总代码量约200万行（含35万个定理）。
- 历史上最大的单形式化项目（如Feit-Thompson定理）耗时约10年，代码量仅为Gauss的 10倍量级。
- 关键突破：Gauss成功形式化了复分析中 人类尚未完全编码的缺失结果，直接打通了PNT证明的最后障碍。
3. 为什么Gauss比人类更快？
- 不知疲倦：AI可以24/7连续工作，无需休息或会议讨论。
- 优化目标单一：Gauss被严格训练为”以最快速度完成形式化”，而人类团队还需兼顾教学、协作、探索其他数学问题。
- 新算法优势：Math公司可能采用了 强化学习+大语言模型（LLM） 的混合架构，让Gauss能自主推理并优化证明路径。
陶哲轩的反思：AI时代，数学研究的目标变了
面对Gauss的成就，陶哲轩在Mastodon上撰文，深刻反思了 形式化项目的本质：
“过去，人类主导的形式化项目往往‘顺便’实现了许多隐性目标（如培养社区、优化代码结构）。但AI工具可能 只优化明确目标，而忽略其他重要方面。”
他提出了一个关键警示：
- 古德哈特定律的启示：当AI被训练去”完成形式化证明”时，它可能牺牲 代码可读性、数学库兼容性、教育价值 等隐性目标。
- 未来项目的挑战：组织者必须 明确所有目标（包括未明说的），并协调AI与人类的分工。
Math公司：从BatchNorm到AI数学革命的幕后推手
Gauss背后的公司 Math，其创始人 Christian Szegedy 是AI界的传奇人物：
- 2015年ICML时间检验奖得主：他与Sergey Ioffe提出的 Batch Normalization（批归一化），让深层神经网络训练效率大幅提升，引用超6万次，是深度学习普及的关键技术。
- 新目标：可验证的超级智能：Szegedy的团队计划在未来12个月内，将Gauss的形式化代码量提升 100~1000倍，目标是构建 “通才型机器数学家”，最终走向 “可验证的超级智能”。
未来展望：AI数学家将如何改变科学？
- 数学研究加速：Gauss证明，AI可在 复杂数学领域（如数论、拓扑） 实现指数级效率提升，未来可能解决更多”人类长期卡壳”的猜想（如黎曼假设）。
- 科学验证革命：形式化不仅是数学工具，还可用于 物理定律、生物模型 的严格验证，减少错误（如NASA火星气候探测器的软件bug悲剧）。
- 人机协作新范式：数学家将不再手动编写证明细节，而是 指导AI探索方向，专注于更高层次的洞察。
欢迎来到”硅基高斯”的时代
Gauss的成功不仅是技术突破，更是一个象征——数学的圣殿正在向AI敞开大门。正如陶哲轩所言：”我们需要重新定义科学项目的目标。” 而Christian Szegedy的Math公司，或许正站在 AI+数学革命 的潮头。
下一步，我们期待Gauss挑战更难的猜想（如ABC猜想），并开源其技术细节。 科学的未来，已不再是人类孤独的探索，而是 人机共生的智慧交响曲。