陶哲轩团队1年半项目，被他3周搞定，曾与LeCun吵翻天，如今AI大佬创业用智能体震惊整个学界？

刚刚，xAI前联合创始人、MorphLabs首席科学家ChristianSzegedy宣布了自己创业的消息。其创立的新公司MathInc.已然上线，是一家致力于通过自动形式化技术打造可验证超级智能的新公司。Szegedy表示，基于其在MorphLabs开发的强大RL基础设施，MathInc.已经通过其新的自动形式化智能体Gauss完成了强素数定理的形式化，并取得突破性成果。

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

据MathInc.团队介绍，Gauss是首款专为协助数学专家开展形式化验证工作打造的自动形式化智能体。借助Gauss，他们已成功完成2024年1月由菲尔兹奖得主陶哲轩（TerenceTao）与AlexKontorovich提出的挑战，即在Lean定理证明器中完成强素数定理（PrimeNumberTheorem,PNT）的形式化工作。目前，相关代码已上传至GitHub。

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

将人类数学成果转化为可验证的机器代码，长期以来一直是一项重大挑战。然而，该过程成本极高——不仅需要稀缺的专业人才，推进难度也远超预期。例如，陶哲轩与AlexKontorovich团队在投入18个月努力后，才于2025年7月宣布取得阶段性进展，而复分析领域的核心难题始终是阻碍他们实现目标的关键瓶颈。

正是在这一背景下，MathInc.团队宣布，借助Gauss智能体，他们仅用三周时间便完成了这一项目。Gauss可实现数小时的自主运行，大幅减少了以往仅由顶尖形式化专家才能承担的工作量。在此过程中，Gauss还完成了复分析领域关键缺失成果的形式化，为以往被认为“难以触及”的未来研究方向扫清了障碍。

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

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

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

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

“Gauss的问世，让我们得以窥见形式化技术未来的规模化发展方向。目前，Gauss仍需依赖数学专家提供的自然语言框架，且在该框架的搭建与优化上需高水平专家指导。但我们预计，未来版本的Gauss将具备更强的能力与更高的自主性。”

据MathInc.称，他们已启动技术部署工作，旨在为一线数学家与证明工程师提供实用工具。现在，他们正与部分数学家群体接洽，推进beta测试。

数论家、斯坦福大学数学系斯泽格教授助理JaredDukerLichtman表示，“与Gauss合作，我感受到了人机协作的新范式，特别是对于那些关心数学验证但又不会自己编程的人来说。随着时间的推移，这可能会开启人类与计算机之间数学的黄金时代。”物理学家JoseAliVivas称赞道，“令人惊叹的Gauss智能体。”威斯康星大学计算机科学教授PedroDomingos评价道，“不要将‘深度学习不能做数学’与‘人工智能不能做数学’混淆。人工智能天生就会做数学。”

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

MathInc.透露，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编程初创公司MorphLabs担任首席科学家。这家公司的目标是：实现“可验证的超级智能”。

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

2015年，深度学习界面临一个棘手的问题：训练深层神经网络既困难又极具挑战。当时，还是谷歌研究员的Szegedy与另一位谷歌研究员SergeyIoffe找到了问题的关键。他们共同发表了一篇论文，标题是《BatchNormalization:AcceleratingDeepNetworkTrainingbyReducingInternalCovariateShift》。这篇论文提出了一种名叫“批归一化”（BatchNormalization，简称BN）的技术，彻底改变了深度学习的训练方式。

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

参考链接：

https://www.math.inc/gauss

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