AI形式化验证246定理，25岁创始人创首次突破
一项由人类数学家完成的素数领域核心定理，刚刚由AI系统完成了全流程的形式化验证，最终确认证明严谨无误，逻辑链条完整。
2026年8月17日，Axiom Math这家AI企业宣布，其自研的AxiomProver系统完成了246定理的形式化验证工作。
所谓246定理，其核心内容是：无论数值规模多大，总能找到一对间距不超过246的素数。尽管距离孪生素数猜想的终极目标——间距为2的素数对——仍有不小差距，但这已经是当前学界最接近该猜想的研究成果。
246这个数字的由来
这一成果的背后，是数论领域数十年的研究积累。孪生素数猜想自19世纪提出以来，一直悬而未决，其核心猜测是存在无穷多对相差为2的素数，比如3和5、11和13这类组合，虽然随着数值增大素数越来越稀少，但这类配对应该始终存在。
2013年，数学家张益唐打破了这一僵局。当时已年近58岁的他，彼时只是新罕布什尔大学的一名讲师，此前曾有过在快餐店工作、协助朋友打理旅馆的经历。他的研究证明了存在无穷多对间距不超过7000万的素数，为这个百年难题打开了突破口。
之后，牛津大学的James Maynard提出了全新的研究方法，直接将这个间距上限从7000万压缩到了600，这一成果也让他在2022年斩获了菲尔兹奖。
随后，Maynard与菲尔兹奖得主陶哲轩联手，联合全球顶尖数论学者组成Polymath8b协作团队，通过在线接力的方式进一步将间距上限推进到了246。在之后的十多年里，这一数值始终没有被进一步缩小。
AxiomProver的验证流程
此次AxiomProver完成的并非定理的原创证明，而是将人类数学家已有的证明转化为机器可自动检查的形式化语言。这套系统是一个多智能体协作系统，由四个核心模块闭环完成整个转化流程：
- Auto-formalizer模块负责将论文中被标注为“显然”“易验证”的跳步补全，转换为Lean 4编程语言代码；
- Conjecturer模块自动生成证明过程中缺失的中间引理；
- 核心引擎负责搜索完整的证明路径；
- Auto-informalizer模块则将机器生成的证明翻译为自然语言，方便人类数学家进行审核。
此次验证的246定理证明文档长达132页，分为14个章节，从最基础的算术函数定义开始，逐步搭建起完整的证明体系。其底层采用了GPY方法（Goldston-Pintz-Yıldırım方法），并在Maynard的研究基础上发展出多维筛法，将问题转化为一个50维的优化问题。
具体来说，研究团队设定参数k=50、ε=1/25，在50维空间中构建权重函数，这50个维度对应的正是一组可容许50元组，即50个精心挑选的非负整数，其最大值与最小值的差恰好为246，这也是246这个数值的最终来源。
验证可容许50元组的方法相对直接：只需检查所有不超过50的素数（共15个），确认这50个数对每个素数p取模后，不会覆盖p的全部剩余类。
整个证明中最关键的数值是M₅₀,₁/₂₅ > 4.0043，这是一个通过在50维扩大单纯形上对profile函数F求解优化问题得到的变分常数。证明的逻辑链条为：如果该变分常数M大于2/ϑ（其中ϑ是素数在算术级数中的分布水平，根据Bombieri-Vinogradov定理，ϑ<1/2，因此2/ϑ约等于4），就能保证在可容许元组对应的位移中，至少存在两个素数。此次验证中得到的4.0043大于4，因此证明成立。
整个形式化验证过程严格追踪了每个结论的依赖关系，最终仅依赖两个外部定理：Bombieri-Vinogradov定理（关于素数在算术级数中的分布水平）和带误差项的素数定理。其余所有中间结果，从Möbius函数的整除求和恒等式到Mertens偏差估计，全部在系统中从头完成证明。
最终的验证结果通过了Lean 4的严格检查，包括三个核心结论：基于Bombieri-Vinogradov定理证明存在无穷多间距≤600的素数对、证明存在无穷多间距≤246的素数对，以及结合该定理与数值证书证明素数间距不超过246。目前，该验证项目的代码仓库已在GitHub开源，分为PrimeGapsTheory和PrimeGapsCert两个部分，任何人都可以在本地运行lake env comparator命令进行独立验证。
年轻创始人与顶尖团队
Axiom Math这家企业本身的发展历程也颇具话题性。其创始人洪乐潼（Carina Hong）成长于普通家庭，早年通过免费奥数项目接触数学竞赛，高中阶段进入CMO省队。
之后她前往MIT攻读数学与物理双学位，仅用3年就完成了全部学业。本科期间，她发表了9篇同行评审论文，并斩获了本科生数学研究的最高荣誉Morgan Prize。毕业时，她同时收到了普林斯顿、斯坦福、哈佛、MIT的博士录取通知，最终选择了斯坦福大学，但并未完成博士学业。
2025年3月，年仅23岁的她退学创业，成立了Axiom Math，团队成员大多来自Meta FAIR、Google Brain和DeepMind等顶尖AI实验室。
值得关注的是，洪乐潼邀请了自己在MIT时的导师、弗吉尼亚大学数论教授Ken Ono担任创始数学家。Ono是拉马努金研究领域的权威，全程深度参与了246定理的形式化验证工作。
资本对这家初创企业的认可度极高：2025年10月，Axiom Math完成了6400万美元的种子轮融资；2026年3月，又完成了2亿美元的A轮融资，估值达到16亿美元。
成立仅一年的企业能获得如此高的估值，与其技术成果密不可分：AxiomProver在2025年12月的Putnam竞赛中拿到了12题全对的满分成绩，成为该赛事98年来第6个实现完美得分的系统；2026年2月，该系统解决了4个未解数学猜想；同年7月，在IMO赛事中拿下42/42的满分；此次完成246定理的形式化验证，更是其技术实力的重要体现。
技术的长远价值
尽管此次验证的是已有的数学证明，但Ken Ono更关注的是这项技术背后的安全价值。当前，AI正在大规模生成代码，这些代码的产出速度远超人类的审查能力，未来全球范围内将有大量无人阅读过的代码投入运行。
而数论正是现代密码学的基石，RSA加密、椭圆曲线加密等技术都基于数论原理。此次用于验证数学证明的形式化技术，未来可以直接用于验证AI生成的代码是否正确合规。在Ono看来，形式化证明正是应对这一挑战的理想试验场。
目前AI尚无法独立创造全新的数学，但Axiom Math的技术路线避开了这一限制，通过验证人类已有的创造来体现价值——验证比创造更容易，但验证本身的价值同样不可估量。
