AxiomProver 自动验证「246 定理」，AI 形式化数学证明迎里程碑

Axiom Math 公司宣布，其自主研发的多 Agent 形式化验证系统 AxiomProver 已首次自动完成对「246 定理」的形式化验证。该定理属于数论中关于素数间隔的重要结果，长期被视为人类素数研究的前沿。Axiom Math 创始数学家 Ken Ono 表示：「这条定理当前代表了人类关于素数知识的边界。」此次验证不仅是 AI 辅助数学研究的一次标志性突破，也展示了 AI 在未来为 AI 生成代码提供形式化安全保障的可能性。

AxiomProver 与可复用的形式化成果

这并非 AxiomProver 第一次进入公众视野。年内，Axiom Math 已借助这一多 Agent 系统破解了多道未解的数学难题，并形式化验证了大量数学证明。然而，「246 定理」的形式化是该系统迄今最具分量的成就。值得注意的是，团队在本次工作中特意让形式化的各个组件可被后续任务复用，并围绕「素数间隔」构建了一个可扩展的形式化结果库，而「246 定理」正是这一库中的旗舰结果。曾参与相关工作的卡内基梅隆大学博士生 Sidharth Hariharan 认为，与此前同类工作相比，这一次的形式化在通用性与可复用性上更为完善。

什么是「246 定理」

「246 定理」可追溯至孪生素数猜想：是否存在无穷多对相差仅为 2 的素数？该猜想由 19 世纪法国数学家 Alphonse de Polignac 正式提出，至今未被完全证明。

• 2013 年，Yitang Zhang 证明了存在无穷多对间隔不超过 7000 万的素数。
• 几个月后，牛津大学教授 James Maynard 利用不同方法把间隔压缩至 600。
• 此后，Maynard 与 UCLA 教授、Fields 奖得主 Terence Tao 等人组成的 Polymath8b 团队进一步将间隔降至 246，这就是「246 定理」的内容。

AxiomProver 此次自动形式化验证的正是这一关键结果。

通往 AI 生成代码的形式化验证

「246 定理」所涉及的数论方法，是现代网络安全与密码学的底层数学基础。Ono 更看重的是其更长远的影响：随着 AI 生成的代码开始广泛应用于基础设施、金融系统和数据保护等领域，如何确保这些代码的正确性，正成为日益紧迫的挑战。

Axiom Math 的设想是，若能将代码的关键性质——例如算法是否终止、程序对任意输入是否输出正确结果——转化为严格的数学命题，那么 AxiomProver 这类形式化验证技术就有望直接对其进行证明，从而为 AI 生成代码的可靠性提供数学级别的保障。

「世界即将运行在无人真正阅读过的代码之上。」Ono 总结道，「AI 已来，我们不能再回避——形式化证明将是解决我认为 AI 时代最重要挑战的试验场。」