25岁广州女孩用AI验成了！两大菲尔兹奖得主心血，无误

新智元报道 人类证出来的最难素数定理，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定理是人类数学家证的，它只负责把证明翻译成机器能检查的形式。 具体来说，这台阅卷机器是一个 多智能体系统 ，由四个模块闭环协作、自主完成转化。 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 年近六旬数论教授 给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 编辑：摩西 秒追ASI ⭐ 点赞、转发、在看一键三连 ⭐ 点亮星标，锁定新智元极速推送！ 文章原文