整理 | 华卫

刚刚，xAI 前联合创始人、Morph Labs 首席科学家 Christian Szegedy 宣布了自己创业的消息。其创立的新公司 Math Inc. 已然上线，是一家致力于通过自动形式化技术打造可验证超级智能的新公司。Szegedy 表示，基于其在 Morph Labs 开发的强大 RL 基础设施，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 的死穴，无论未来采用多强大的算力，多广阔和优质的数据集训练 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。十年后，这篇论文还在今年的国际机器学习大会（ICML）2025 上，被授予了“时间检验奖”（Test of Time Award）。

参考链接：

https://www.math.inc/gauss

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

声明：本文为 AI 前线整理，不代表平台观点，未经许可禁止转载。