刚刚，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。 据 Math Inc. 称，他们已启动技术部署工作，旨在为一线数学家与证明工程师提供实用工具。现在，他们正与部分数学家群体接洽，推进 beta 测 ...

Core Viewpoint - Math Inc. has launched a new automated formalization agent named Gauss, which has successfully formalized the Prime Number Theorem in a significantly shorter time compared to traditional methods, showcasing the potential of AI in mathematical verification [2][4][5]. Group 1: Company Overview - Math Inc. was founded by Christian Szegedy, a former co-founder of xAI and chief scientist at Morph Labs, focusing on creating verifiable superintelligence through automated formalization technology [2][12]. - The company has developed Gauss, the first automated formalization agent designed to assist mathematicians in formal verification tasks [4][10]. Group 2: Technological Achievements - Gauss completed the formalization of the Prime Number Theorem in just three weeks, a task that previously took a team 18 months to achieve [5][6]. - The agent generated approximately 25,000 lines of Lean code, including over 1,000 theorems and definitions, marking a significant milestone in formal verification [6][10]. - Gauss can autonomously operate for over 10 hours, completing 95% of the formalization and proof work, with human intervention required only for the remaining tasks [8][10]. Group 3: Future Prospects - Math Inc. aims to enhance Gauss's capabilities and autonomy, with plans to significantly reduce the time required for large formalization projects within the next 12 months [10]. - The company is currently engaging with mathematicians for beta testing and aims to provide practical tools for mathematicians and proof engineers [10][9]. Group 4: Academic Recognition - Gauss has received positive feedback from the academic community, with experts highlighting its potential to revolutionize human-computer collaboration in mathematics [9][10].