（来源：新智元）

　　新智元报道

　　人类证出来的最难素数定理，AI刚从头验了一遍。

　　结论是：证明成立，逻辑无误。

　　8月17日，由一位25岁广州女孩创立的AI公司Axiom Math宣布，自家系统AxiomProver完成了「246定理」的形式化验证。

　　论文地址：https://primegaps.axiommath.ai/paper/

　　所谓246定理，指的是无论数字多大，你总能找到两个素数，它们之间的间距不超过246。

　　虽然离终极目标「差距为2」还差着不少，但它已经是目前最接近「孪生素数猜想」的结果了。

　　根据Axiom Math创始数学家Ken Ono的解释：「这个定理，就是人类目前对素数理解的天花板。」

　　那么，这次的验证到底是怎么做的呢？

　　246这个数字怎么来的

　　故事要从孪生素数猜想说起。

　　这是19世纪提出的老问题，猜的是存在无穷多对相差为2的素数。3和5，11和13，17和19，越往后越稀少，但应该永远不会断。

　　漂亮，简洁，但一百多年没人能证。

　　2013年，张益唐打破了僵局。

　　他在Subway做过三明治，在朋友的汽车旅馆帮过忙，发论文那年58岁，还只是新罕布什尔大学的一名讲师。

　　但就是他，证明了存在无穷多对差距不超过7000万的素数。

　　之后，牛津大学的James Maynard又用了一套完全不同的方法，直接把7000万砍到600。而这个贡献也给他送了一座2022年菲尔兹奖。

　　紧接着Maynard又和菲尔兹奖得主陶哲轩联手，拉上一群顶尖数论学家组成Polymath8b协作团队，在线接力，硬是把600推到了246。

　　随后十多年过去，再没有人把这个数字往下挪哪怕一步。

　　AxiomProver到底怎么「验证」的

　　先划个重点：AxiomProver不是在证明新定理。

　　246定理是人类数学家证的，它只负责把证明翻译成机器能检查的形式。

　　具体来说，这台阅卷机器是一个多智能体系统，由四个模块闭环协作、自主完成转化。

　　但真正硬核的，是被验证的数学本身。

　　打开Axiom团队公开的验证论文，整个证明分14个章节共132页，从最基础的算术函数定义一路搭到最终组装。

　　底层用的是GPY方法（Goldston-Pintz-Yıldırım），Maynard在此基础上发展出多维筛，把问题变成了一个50维的优化问题。

　　其中，参数设定为k=50、ε=1/25，在50维空间上构造权重函数。

　　这50个维度对应一个可容许50元组，即一组精心挑选的50个非负整数，最大值减最小值恰好等于246。

　　这就是246这个数字的终极来源。

　　验证可容许性的方法倒是意外地直接。只需要检查所有不超过50的素数（一共15个），对每个素数p，确认这50个数 mod p 后不会覆盖全部剩余类。

　　然后是整个证明里最关键的一个数：M₅₀,₁/₂₅ > 4.0043。

　　这是一个变分常数，通过在50维的enlarged simplex上对profile函数F求解优化问题得到。

　　证明的逻辑链是这样的：如果M大于2/ϑ（ϑ是素数在算术级数中的分布水平，由Bombieri-Vinogradov定理保证ϑ

　　4.0043 > 4。定理成立。

　　整个形式化严格追踪了每个结论的依赖关系，最终只依赖两个外部定理：Bombieri-Vinogradov定理（素数在算术级数中的分布水平）和带误差项的素数定理。

　　其余所有中间结果，从Möbius函数的整除求和恒等式到Mertens偏差估计，全部在库里从头证明。

　　最终输出三个结果，全部通过Lean 4验证：

　　目前，仓库已在GitHub上开源，分成PrimeGapsTheory和PrimeGapsCert两部分。任何人都可以本地跑lake env comparator自己验证。

　　项目地址：https://github.com/AxiomMath/PrimeGapsLib

　　年近六旬数论教授

　　给25岁创始人打工

　　值得一提的是，Axiom Math这家公司本身就是一篇故事。

　　创始人洪乐潼（Carina Hong）出生在一个普通家庭。小时候通过一个免费的奥数项目开始接触竞赛，高中进了CMO省队。

　　后来她去了MIT读数学和物理双学位，3年修完。

　　本科期间发了9篇同行评审论文，一举拿下了本科生数学研究的最高荣誉——Morgan Prize。

　　毕业时被普林斯顿、斯坦福、哈佛、MIT同时录取读博。她选了斯坦福。但没读完。

　　2025年3月，23岁的洪乐潼退学创业，成立Axiom Math。团队来自Meta FAIR、Google Brain和DeepMind。

　　但真正让圈内人侧目的，是她把自己在MIT时的导师、弗吉尼亚大学数论教授Ken Ono招来当了「创始数学家」。

　　Ono是拉马努金研究领域的权威，246定理的形式化工作他全程深度参与。

　　资本的嗅觉也很灵。2025年10月，种子轮拿了6400万美元。2026年3月，A轮又融了2亿美元，估值直接冲到16亿美元。

　　一家成立刚满一年的公司，凭什么值16亿？

　　把AxiomProver的成绩单拉出来看一眼就知道了。

　　2025年12月Putnam竞赛12题全对满分，98年来第6个完美成绩；2026年2月解决4个未解猜想；7月IMO拿下42/42满分；8月，246定理形式化验证完成。

　　验证数学只是开始

　　但比起这张成绩单，Ken Ono最在意的其实不是数学本身，而是数学背后的安全问题。

　　AI正在大规模生成代码，渗透进金融、医疗等关键系统。

　　这些代码的产出速度远超人类审查的能力，全世界即将运行大量没有人读过的代码。

　　而数论恰恰是现代密码学的基石，RSA、椭圆曲线，底层全是数论。

　　今天用来验证数学证明的形式化技术，明天就能用来验证AI写的代码是否正确。

　　在Ono看来，形式化证明正是应对这一挑战的试验场。

　　AI目前还造不出新数学，但Axiom做的事恰恰绕开了这个限制，不需要AI创造，只需要它检查人类的创造是否正确。

　　验证比创造容易，而验证本身价值同样巨大。

　　参考资料：

　　https://primegaps.axiommath.ai/paper/

　　https://spectrum.ieee.org/axiom-math-246-theorem-formalization

　　编辑：摩西