AI验证“246定理”，陶哲轩呼吁数学家主动引领AI

2、3、5、7、11、13、17、19是彼此靠近的几个素数，其中，3和5、5和7、11和13、17和19这几组素数都相差2。离0越远，这些孪生素数出现得越稀少，但仍然会偶有出现。

经过数学家们的集体接力，目前已证明存在无穷多对相差246的素数。这一“246定理”的已知结果日前被AI创业公司Axiom Math的人工智能系统验证为正确，据《IEEE Spectrum》8月17日报道，这项AI技术未来或可用于检验AI生成代码的正确性。

人工智能正在重塑无数领域，数学也不例外。在谈到AI能对孪生素数研究产生的影响时，今年5月，国际知名数学家张益唐表示，目前在数论或经典解析数论的问题上，AI还无能为力，但AI能力很强，可能很快能学会足够的知识。解析数论积累了很多文献，那些文献现在看不过来，但都是证明出来的对的结果。这些有可能让AI再概括、回顾一下，也许能在里面发掘出很多新的东西。

“我们不妨假设，不久之后AI就能成功完成相当一部分数学任务。”菲尔兹奖得主、著名数学家陶哲轩7月份在2026年国际数学家大会上表示，“如果以这一前提为条件，就会清楚地看到，我们现在必须思考我们的目标和价值观。”

孪生素数猜想

孪生素数猜想最早由法国数学家Alphonse de Polignac在19世纪精确表述。该猜想认为，无论沿着数轴走多远，孪生素数仍会不断出现。换言之，存在无穷多个素数对，使得两素数的差为2。

在1900年的国际数学家大会上，数学家希尔伯特发表著名演讲，提出了23个有待解决的重要数学难题和猜想，其中“孪生素数猜想”是第8个问题中的一个小问题，被认为是数论史上的经典难题。

孪生素数猜想和负有盛名的黎曼猜想、哥德巴赫猜想一道成为希尔伯特第8问题中的一部分，尽管叙述简单，但这一古老猜想至今未被证明。

直到2013年，张益唐证明，存在无穷多对间隙小于7000万的相邻素数对。当年5月，张益唐在纯粹数学领域知名刊物《数学年刊》上发表《素数间的有界距离》，证明了存在无数多个素数对（p, q），其中每一对素数之差，即p和q的距离，不超过7000万。这在数学史上第一次实质性推进解决“孪生素数猜想”。

在张益唐公布一周之后，全球数学家开始争相寻找最小的数字。几个月后，牛津大学教授詹姆斯·梅纳德（James Maynard）采用另一种方法，将这一界限从7000万压缩至600，这项成就为他后来获得2022年菲尔兹奖做出了重要贡献。

后来，梅纳德和陶哲轩一起，将间隙进一步缩小至246。“246定理”也就是存在无穷多对相差246的素数，这是数学家们迄今最接近目标间隙2的结果。但孪生素数猜想本身，也就是相差恰好为2的素数，至今仍未被证明。

“再往下就会有很多问题。”陶哲轩曾说，“需要越来越多的电脑程序，当然也有理论问题。用现有的方式，我们不能得出更好的结果了，因为有所谓的平等问题，没有人知道怎么解决这个问题。”

形式化证明

Axiom Math创始数学家Ken Ono（小野健）表示，246定理“目前代表了人类关于素数知识的边界”。这一定理也被Axiom Math的人工智能系统AxiomProver验证为正确。

数学家撰写的非形式化证明中，充满了直觉性的跳跃与手势式的示意，读者需要自行补全空白。而在形式化证明中，哪怕只有一个微小的错误，也会把整个论证彻底打回。不过，一旦论证顺利通过编译，也能建立起真正的严谨性。

在形式化证明中，数学家会让计算机检查一个机器可读版本的证明。小野健曾经在和陶哲轩的一次对谈中坦言，自己第一次看到数学家们去形式化那些早已确立的初等本科数学结果时，本能反应是怀疑，他怀疑为何要重新证明这些已经解决的本科数学，而不是训练学生攻克全新的开放问题。

而今年，Axiom Math已利用多智能体系统将数学命题转化为机器可检查的证明，破解了数个未解数学问题，并验证了更多证明，其中就包括“246定理”的验证。

数论是支撑当今网络安全和密码学的数学分支，形式化技术在数论中至关重要，未来有望用于验证保护数据安全的具体方法。小野健将数学形式化证明视为通往验证AI生成代码的垫脚石，“世界即将运行在没人读过的计算机代码上。”

这些AI生成代码正开始被用于运行基础设施、财务管理和保护数据的各类系统中。如果代码的性质能够被转化为精确的数学命题，例如算法是否会终止、程序对任意输入的输出是否正确等，那么AxiomProver技术可以对它们开展形式化证明，验证AI生成代码的正确性，让代码更加安全可用。

仅生成和验证证明远远不够

小野健曾是美国弗吉尼亚大学数学系讲席教授，辞去教职后，去年57岁的他加入了学生洪乐潼创办不久的AI公司Axiom Math，让“AI数学家”从科幻变成现实。小野健说，“AI已经到来，我们不能再视而不见。形式化证明是解决我认为我们将面临的最重要AI挑战的试验田。”

数学的解题分为几个不同阶段，首先是给出证明并加以验证。在今年7月举办的2026年国际数学家大会上，陶哲轩表示，AI在这方面相当擅长。大模型通常能生成候选证明或关键思路，而AI系统也能严谨检查冗长或复杂的证明。问题出现在下一阶段，即人类对证明的评价和解释。

人类可以得到长达十万行的证明并需要加以验证，“但没人能理解它们。”据西蒙斯基金会（Simons Foundation）消息，陶哲轩表示，即便是输入提示词生成证明的人也可能不理解它们。“仅仅生成和验证证明是不够的。证明必须被充分解释，以便能在学术共同体中传播和被理解。”如果一个证明无人能懂，那么它被接受的可能性就微乎其微。

“展示过程，并描述你是如何得出结论的，哪些方法有效，哪些无效，以及你采取了什么方式。”他表示，过去并不强调过程，而是让结果自己说话。这种方法一直有效，“直到我们意识到可以自动化结果而不必经过过程，目前的（AI）工具对其过程却极为模糊。”

如果没有这些步骤，一个结果就无法被经典化、写进教科书。“如果你希望某个数学领域对工程师、物理学家或其他领域的人有用，他们不会去翻《数学年刊》上的最新论文，他们需要的是教科书。数学最有价值的应用，只有在达到这种状态之后才能真正释放出来。”陶哲轩表示，AI本身的存在也离不开这些教科书。

他呼吁数学家们主动引领，将AI融入数学，而非被动应对。“在有些地方我们应该使用AI，但我们应该主动采取行动，决定哪些地方该用。我们制定规则，界定什么是可接受的、什么不是，我们不应让外部力量为我们界定这些。”

澎湃新闻记者 张静