Axiom Math 团队宣布，他们使用自主研发的 AI 系统 AxiomProver，首次自动验证了数论中著名的“246 定理”的证明。该定理指出，存在无穷多对相差 246 的素数。这一成果被视为 AI 辅助数学研究的一个重要里程碑，标志着 AI 在形式化验证领域迈出了关键一步。
形式化验证是一种让计算机检查机器可读版本证明的方法。虽然这一过程并非 100% 保证证明正确——正如近期一项演示所揭示的，方法中的缺陷可能被利用来接受错误的 AI 生成证明——但计算验证仍被数学家视为最接近“橡皮图章”式的确认方式。Axiom Math 表示，此次验证不仅形式化了一个重要的数论进展，更展示了未来如何利用自动化 AI 验证来确保 AI 生成的计算机代码的正确性，这些代码即将支撑全球的软件系统。
这并非 AxiomProver 的首次成功。Axiom Math 已使用其自主多智能体系统，将数学陈述转化为机器可检查的证明，今年已攻克多个未解数学问题并验证了更多证明。但 246 定理的形式化是迄今最具意义的成果。Axiom Math 创始数学家 Ken Ono 表示：“这个定理目前代表了人类对素数认知的阈值。”
此前，Axiom Math 的竞争对手 Math, Inc. 曾使用其 Gauss 代理，形式化了 Maryna Viazovska 2022 年菲尔兹奖获奖证明——8 维和 24 维球体堆积问题。卡内基梅隆大学博士生 Sidharth Hariharan 曾领导人类团队制定 Viazovska 证明的形式化蓝图，他认为 246 定理的形式化是更全面、更有用的成就。Hariharan 现为 Axiom Math 实习生，深度参与了 246 定理证明的形式化工作。他指出，与一次性处理单一问题不同，Axiom Math 明确致力于使形式化的组件可重复用于其他形式化任务和数学研究。团队利用 AxiomProver 构建了一个关于素数间隙的结果库，246 定理是该库中的旗舰成果。
“246 定理”源于孪生素数猜想。该猜想由法国数学家阿尔方斯·德·波利尼亚克在 19 世纪首次精确表述，认为存在无穷多对相差 2 的素数（孪生素数）。尽管表述简单，但该猜想至今未被证明。2013 年，张益唐（现为广州中山大学教授）证明了存在无穷多对相差 7000 万的素数，首次取得突破。几个月后，牛津大学教授 James Maynard 用不同技术将这一差距从 7000 万大幅缩小到 600，这一成就为他赢得 2022 年菲尔兹奖做出了重要贡献。作为 Polymath8b 合作组织成员，Maynard 和菲尔兹奖得主、加州大学洛杉矶分校教授 Terence Tao 将差距进一步缩小到 246，这是数学家们最接近目标差距 2 的一次。AxiomProver 验证的正是这个“246 定理”——存在无穷多对相差 246 的素数。
这项工作的意义不仅限于数论。数论是现代密码学和网络安全的基础，因此形式化验证可能有助于未来验证我们保护数字数据的具体方式。但 Ken Ono 更看重更宏大的图景：他将形式化数学证明视为验证 AI 生成代码的垫脚石。随着 AI 生成的代码开始应用于社会各个领域，如基础设施运行、金融管理和数据保护，其安全性备受关注。如果代码的属性（如算法是否终止、程序输出对任何输入是否正确）能被转化为精确的数学陈述，那么源自 AxiomProver 的技术将非常适合正式陈述并证明这些属性。这样一来，数学上验证 AI 生成代码的正确性将使这些代码可以安全使用。Ono 总结道：“世界即将运行在没人读过的计算机代码上。AI 已经到来，我们不能再视而不见——证明形式化是解决我认为我们将面临的最重要挑战的试验场。”