AI 在数学领域的研究取得新进展！ 近日，一家名为 Math, Inc. 的公司宣称利用 Gauss 智能体，已经完成了一个关乎 8 维和 24 维空间中的最优球体堆积定理的形式化证明，代码量约为 20 万行 （LOC）。 这一定理最初由数学家玛丽娜・维亚佐夫斯卡（Maryna Viazovska）及其合作者证明，Maryna Viazovska 也凭此荣获 2022 年国际数学家大会菲尔兹奖。 据悉， 这是本世纪唯一一个被完全形式化证明的菲尔兹奖成果，也是历史上规模最大的单一用途 Lean 形式化项目。 而背后的这家名为 Math, Inc. 的公司，也不是第一次完成数学问题的形式化证明了。 资料显示，Math, Inc. 是由 xAI 前联合创始人、Morph Labs 首席科学家 Christian Szegedy 创立，致力于通过自动形式化技术打造可验证超级智能，Gauss 则是首款 专为协助数学专家开展形式化验证工作打造的自动形式化智能体。 去年， Gauss 只用了三周时间，就完成了陶哲轩和 Alex Kontorovich 提出的数学挑战， 即在 Lean 定理证明器中完成强素数定理（Prime ...

刚刚，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].