Math Inc.推出Gauss智能体，引领数学验证新时代

近日，xAI 前联合创始人、Morph Labs 首席科学家 Christian Szegedy 宣布创立新公司 Math Inc.，致力于通过自动形式化技术打造可验证超级智能。Szegedy 表示，Math Inc. 已通过其新的自动形式化智能体 Gauss 完成了强素数定理的形式化，并取得突破性成果。

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

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

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

将人类数学成果转化为可验证的机器代码是一项重大挑战。然而，该过程成本极高，不仅需要稀缺的专业人才，推进难度也远超预期。Math Inc. 团队宣布，借助 Gauss 智能体，仅用三周时间便完成了这一项目。

此外，通过 Gauss，该团队生成了约 2.5 万行 Lean 代码，其中包含 1000 余个定理与定义。从历史角度看，如此规模的形式化证明历来是重要里程碑。

Szegedy 在 X 平台澄清道，“我认为没有任何地方声称我们重新完成了原项目耗时 18 个月才完成的工作。”他相信 Gauss 在处理速度上能达到相近的处理速度。

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

“Gauss 的问世，让我们得以窥见形式化技术未来的规模化发展方向。”据 Math Inc. 称，他们已启动技术部署工作，旨在为一线数学家与证明工程师提供实用工具。

Jared Duker Lichtman、Jose Ali Vivas 和 Pedro Domingos 等学术界人士纷纷对 Gauss 表示赞赏，认为它开启了人类与计算机之间数学合作的新时代。

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

Szegedy 是深度学习领域的杰出人物。在谷歌工作期间，他领导的 Google N2Formal 团队提出了“批归一化”技术，彻底改变了深度学习的训练方式。

这项技术使得训练深度超过几十层的网络成为可能，并广泛应用于主流卷积神经网络和其他模型中。如今，Szegedy 又将这一创新带到了 Math Inc.，推动数学验证技术的发展。