新智元报道
新智元报道
人类证出来的最难素数定理，AI刚从头验了一遍。
结论是：证明成立，逻辑无误。
8月17日，由一位25岁广州女孩创立的AI公司Axiom Math宣布，自家系统AxiomProver完成了「246定理」的形式化验证。
论文地址：https://primegaps.axiommath.ai/paper/
所谓246定理，指的是无论数字多大，你总能找到两个素数，它们之间的间距不超过246。
虽然离终极目标「差距为2」还差着不少，但它已经是目前最接近「孪生素数猜想」的结果了。
根据Axiom Math创始数学家Ken Ono的解释：「这个定理，就是人类目前对素数理解的天花板。」
那么，这次的验证到底是怎么做的呢？
故事要从孪生素数猜想说起。
这是19世纪提出的老问题，猜的是存在无穷多对相差为2的素数。3和5，11和13，17和19，越往后越稀少，但应该永远不会断。
漂亮，简洁，但一百多年没人能证。
2013年，张益唐打破了僵局。
他在Subway做过三明治，在朋友的汽车旅馆帮过忙，发论文那年58岁，还只是新罕布什尔大学的一名讲师。
但就是他，证明了存在无穷多对差距不超过7000万的素数。
之后，牛津大学的James Maynard又用了一套完全不同的方法，直接把7000万砍到600。而这个贡献也给他送了一座2022年菲尔兹奖。
紧接着Maynard又和菲尔兹奖得主陶哲轩联手，拉上一群顶尖数论学家组成Polymath8b协作团队，在线接力，硬是把600推到了246。
随后十多年过去，再没有人把这个数字往下挪哪怕一步。
先划个重点：AxiomProver不是在证明新定理。
246定理是人类数学家证的，它只负责把证明翻译成机器能检查的形式。
具体来说，这台阅卷机器是一个多智能体系统，由四个模块闭环协作、自主完成转化。
-
Auto-formalizer把论文里那些「显然」「容易验证」的跳步，一步步补全成Lean 4代码；
-
Conjecturer自动生成缺失的中间引理；
-
核心引擎搜索完整证明路径；
-
Auto-informalizer反过来把机器证明翻译成人话，方便数学家审核。
但真正硬核的，是被验证的数学本身。
打开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定理保证ϑ<1/2，此时2/ϑ约等于4），就能保证在可容许元组对应的位移中，至少有两个是素数。
4.0043 > 4。定理成立。
整个形式化严格追踪了每个结论的依赖关系，最终只依赖两个外部定理：Bombieri-Vinogradov定理（素数在算术级数中的分布水平）和带误差项的素数定理。
其余所有中间结果，从Möbius函数的整除求和恒等式到Mertens偏差估计，全部在库里从头证明。
最终输出三个结果，全部通过Lean 4验证：
-
Bombieri-Vinogradov定理 ⇒ 无穷多差距≤600的素数对
-
Bombieri-Vinogradov定理 ⇒ 无穷多差距≤246的素数对
-
Bombieri-Vinogradov + 数值证书 ⇒ 差距≤246
目前，仓库已在GitHub上开源，分成PrimeGapsTheory和PrimeGapsCert两部分。任何人都可以本地跑lake env comparator自己验证。
项目地址：https://github.com/AxiomMath/PrimeGapsLib
值得一提的是，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
编辑：摩西
