AI首次自动验证数学史上最难证明之一——“246定理”

Axiom Math团队利用其AI系统AxiomProver，首次自动验证了一项与素数相关的定理证明，该定理被称为"246定理"，标志着AI辅助数学研究取得重要里程碑。

在形式化验证领域，数学家通常让计算机检查一个可被机器读取的证明版本。这一过程并非百分之百保证证明正确，此前已有研究表明，该方法中存在的漏洞可能被利用，导致系统接受一个由AI生成的错误证明。尽管如此，计算机验证仍是目前最接近"盖章认可"的方式。

此次验证在数论领域具有重要意义。除了这一具体证明本身，它还展示了自动化AI验证未来如何被应用于确保AI生成代码的正确性——这类代码即将成为全球软件系统的底层基础。

这并非AxiomProver初次亮相。Axiom Math已将其自主多智能体系统用于将数学命题转化为机器可验证的证明，今年已攻克多个未解数学难题，并验证了更多证明。但246定理的形式化验证是迄今最具分量的成果。Axiom Math创始数学家肯·奥野表示："这一定理代表着人类关于素数知识的当前边界。"

今年早些时候，Axiom Math的竞争对手Math, Inc.利用其Gauss智能体，将玛丽娜·维亚佐夫斯卡获得2022年菲尔兹奖的球堆积问题证明进行了形式化处理。卡内基梅隆大学博士生西达尔斯·哈里哈兰曾主导维亚佐夫斯卡证明形式化蓝图的人工工作，他认为246定理的形式化是一项更全面、更具实用价值的成就。

目前已在Axiom Math担任实习生的哈里哈兰深度参与了246定理证明的形式化工作。他指出，此次工作的一大区别在于：这并非针对单一问题的一次性处理，Axiom Math明确致力于使形式化过程中的各个模块可被复用于其他形式化任务和数学研究。团队借助AxiomProver构建了一个关于素数间隔的结果库，246定理是该库中最核心的成果。

最初的几个素数彼此相邻：2、3、5、7、11、13、17、19、23、29、31……其中有多对素数之差恰好为2，例如：3与5、5与7、11与13、17与19……

这些相差为2的素数对被称为"孪生素数"。孪生素数随数字增大而变得愈发稀少，但偶尔仍会出现。孪生素数猜想由法国数学家阿方斯·德·波利尼亚克于19世纪首次明确提出，认为无论在数轴上走多远，孪生素数都会持续出现，即孪生素数有无穷多对。

这一易于表述却至今未被证明的猜想，直到2013年才迎来首次实质性突破。现任职于中国广州中山大学的数学家张益唐证明了存在无穷多对素数之差不超过7000万。数月后，牛津大学教授詹姆斯·梅纳德采用不同方法，将这一间隔从7000万大幅压缩至600，这一成就为他赢得了2022年菲尔兹奖——数学界公认的最高荣誉。

随后，在被称为"Polymath8b协作组"的数学家群体中，梅纳德与同为菲尔兹奖得主、加州大学洛杉矶分校教授陶哲轩合作，将间隔进一步缩小至246，这也是数学家迄今最接近目标间隔"2"的结果。正是这一246定理——即存在无穷多对差值为246的素数——被AxiomProver验证为正确。

此次形式化工作所涉及的技术在数论领域具有重要价值，而数论正是当今所有网络安全和密码学的数学基础。因此，这些技术未来或将在验证数字数据安全机制方面发挥重要作用。

然而，Axiom Math的奥野对更宏观的前景更感兴奋。他认为，数学证明的形式化是通往验证AI生成代码的垫脚石。AI生成的代码正越来越多地被应用于支撑基础设施运营、金融管理和数据保护等关键系统，尽管幻觉、漏洞及其他意外安全隐患的风险依然存在。

如果代码的某些属性——例如某算法是否会终止、某程序的输出对任意输入是否正确——能够被转化为精确的数学命题，那么基于AxiomProver衍生出的技术将非常适合对这些属性进行形式化表述与证明，从而从数学层面验证AI生成代码的正确性，使其可以安全使用。

奥野总结道："这个世界即将运行在无人阅读过的代码之上。AI已经到来，我们无法再回避——证明形式化正是解决我认为AI带来的最重要挑战的试验场。"

Q&A

Q1：246定理是什么？为什么它在数学上很重要？

A：246定理指的是存在无穷多对差值为246的素数，是数学家目前最接近孪生素数猜想（差值为2）的成果。它由梅纳德和陶哲轩在Polymath8b协作组中共同推导得出。Axiom Math创始数学家肯·奥野表示，该定理"代表着人类关于素数知识的当前边界"，是数论领域的重要里程碑。

Q2：AxiomProver是如何验证数学证明的？

A：AxiomProver是Axiom Math开发的自主多智能体系统，能够将数学命题转化为机器可验证的证明。在验证246定理时，团队不仅完成了一次性的证明验证，还构建了一个关于素数间隔的可复用结果库，使相关模块可以被应用于其他数学形式化任务，提高了验证工作的系统性和实用价值。

Q3：AI验证数学证明和保障代码安全有什么关联？

A：如果AI生成代码的特定属性（如算法是否终止、输出是否正确）能被转化为数学命题，AxiomProver这类技术就可以对这些属性进行形式化验证，从数学层面确保代码的正确性与安全性。Axiom Math创始数学家奥野认为，证明形式化是解决"世界将运行在无人阅读过的AI代码之上"这一重大挑战的关键路径。