Math Inc. 推出 Gauss 智能体，三周实现强素数定理形式化突破

近日，xAI 前联合创始人兼 Morph Labs 首席科学家 Christian Szegedy 正式宣布其创业项目。他创立的新公司 Math Inc. 已上线，专注于利用自动形式化技术构建可验证的超级智能。Szegedy 透露，借助在 Morph Labs 开发的强化学习基础设施，Math Inc. 通过新型自动形式化智能体 Gauss 成功完成了强素数定理的形式化验证，取得了显著突破。

Gauss：自主工作超10小时的数学智能体 

Math Inc. 团队介绍，Gauss 是首款专为辅助数学专家进行形式化验证设计的自动形式化智能体。利用 Gauss，团队已成功应对了2024年1月由菲尔兹奖得主陶哲轩（Terence Tao）与 Alex Kontorovich 提出的挑战，即在 Lean 定理证明器中实现强素数定理（Prime Number Theorem, PNT）的形式化。相关代码现已公开在 GitHub 上。

存储库链接：https://github.com/math-inc/strongpnt

将人类数学成果转化为机器可验证代码，历来是一项艰巨任务。这一过程不仅依赖稀缺的专业人才，而且进展缓慢、成本高昂。例如，陶哲轩与 Alex Kontorovich 团队历经18个月的努力，才在2025年7月取得阶段性进展，其中复分析领域的核心难题一直是主要障碍。

在此背景下，Math Inc. 团队宣布，借助 Gauss 智能体，他们仅用三周就完成了该项目。Gauss 能够自主运行数小时，大幅降低了以往仅由顶尖形式化专家承担的工作负荷。过程中，Gauss 还形式化了复分析领域的关键缺失成果，为以往被视为“难以实现”的研究方向铺平了道路。

通过 Gauss，团队生成了约2.5万行 Lean 代码，包含1000余个定理与定义。从历史角度看，如此规模的形式化证明标志着重要里程碑，通常需要多年才能完成。即使在最大的单个形式化项目中（这类项目往往耗时十余年，堪称“定义职业生涯”的成果），代码量也仅比此次高一个数量级，最多约50万行。而 Lean 的标准数学库 Mathlib 规模更大，代码量约200万行（含35万个 Lean 定理与定义），由600余名研究者耗时8年共同开发。

随后，Szegedy 在 X 平台进一步澄清：“我认为没有任何声明称我们重新完成了原项目18个月的工作。在我看来，由于新增部分的数学内容极其复杂，我们在已完成部分上的处理速度可能接近原项目。尽管带有推测性，但这一判断可信度很高。因此，我相信借助 Gauss，原项目（中等规模素数定理形式化）本可在1-2周内完成。该系统能自主处理各个模块（每次可持续运行10小时以上，并持续推进工作）。虽然尚未完全自主（无法一次性独立完成整个项目），但在每次迭代中，它通常能自主完成95%的命题形式化与证明，剩余部分需人工介入。对于这些局限，我们始终保持透明。”

此外，Math Inc. 表示，本项目的成功离不开与 Morph Labs 合作开发的 Trinity 环境基础设施。要将 Lean 验证环境扩展到 Gauss 所需规模——支持数千个并发智能体（每个拥有独立的 Lean 运行时），并占用数太字节（TB）的集群内存——是一项复杂的系统工程挑战，而 Morph Cloud 上的 Infinibranch 技术在此发挥了关键作用。

好评如潮，尤获学术界认可 

“Gauss 的出现，让我们看到了形式化技术未来规模化发展的潜力。目前，Gauss 仍依赖数学专家提供的自然语言框架，且框架的搭建与优化需要高水平专家指导。但我们预计，未来版本的 Gauss 将具备更强能力和更高自主性。”

据 Math Inc. 称，他们已开始技术部署，旨在为一线数学家与证明工程师提供实用工具。目前，正与部分数学家群体接洽，推进 beta 测试。

数论家、斯坦福大学数学系斯泽格教授助理 Jared Duker Lichtman 表示：“与 Gauss 合作，我体验到了人机协作的新模式，尤其对于那些关心数学验证但不擅编程的人而言。随着时间的推移，这或许会开启人类与计算机在数学领域的黄金时代。”物理学家 Jose Ali Vivas 称赞道：“令人惊叹的 Gauss 智能体。”威斯康星大学计算机科学教授 Pedro Domingos 评价：“不要将‘深度学习不能做数学’与‘人工智能不能做数学’混淆。人工智能天生就适合做数学。”

有网友评论：“形式验证与人工智能是绝佳组合。生成2.2万行 Lean 代码来证明定理，表明人工智能既能创新又严谨正确。”“有了 Gauss，我们进入了一个新纪元：人工智能与专家携手，加速数学发展，并开启了前所未有的创新与协作可能。”

Math Inc. 透露，Gauss 将大幅缩短大型形式化项目的完成时间。通过进一步的算法优化，目标是在未来12个月内，将形式化代码总量提升2-3个数量级。这一过程将成为全新范式的“试验场”——为“可验证超级智能”及驱动其发展的“机器博学者”奠定基础。

创始人曾改变深度学习历史

揭开 AI 初创公司新篇章的 Szegedy，此前是马斯克旗下人工智能企业 xAI 的12位创始团队成员之一，于2023年5月正式加入。

在 xAI 期间，Szegedy 曾因大语言模型（LLM）的推理能力与 LeCun 公开争论。LeCun 认为，推理能力的缺陷几乎是 LLM 的致命弱点，无论未来采用多强大的算力或数据集，都无法解决。Szegedy 则反驳，卷积网络的推理能力更有限，但这并未影响 AlphaZero 的表现。关键在于推理过程和建立的强化学习（RL）反馈循环。他相信模型能进行深度推理，例如开展数学研究。

2025年6月，Szegedy 成为 xAI 团队首位离职的核心成员，加入 AI 编程初创公司 Morph Labs 担任首席科学家。这家公司的目标是实现“可验证的超级智能”。

更早之前，拥有波恩大学应用数学博士学位的 Szegedy 在谷歌工作十余年，领导 Google N2Formal 团队，专注于深度学习、计算机视觉等领域研究。其学术成果在对抗性样本领域具有里程碑意义，还曾改变深度学习历史。

2015年，深度学习界面临训练深层神经网络的难题：过程困难且极具挑战。当时，作为谷歌研究员的 Szegedy 与同事 Sergey Ioffe 找到了关键。他们共同发表论文《Batch Normalization: Accelerating Deep Network Training by Reducing Internal Covariate Shift》，提出了“批归一化”（Batch Normalization，简称 BN）技术，彻底革新了深度学习训练方式。

在 BatchNorm 出现之前，训练深度超过几十层的网络非常困难。此后，几乎所有主流卷积神经网络（如 ResNet, DenseNet, Inception）和许多其他模型都广泛采用了 BatchNorm。十年后，这篇论文在2025年的国际机器学习大会（ICML）上被授予“时间检验奖”（Test of Time Award）。

参考链接：

https://www.math.inc/gauss

https://www.linkedin.com/in/christian-szegedy-bb284816