AI首次形式化验证246定理 逼近孪生素数猜想

时间：2026年8月17日（IEEE Spectrum 报道），成果对应 Axiom Math 公开的 PrimeGapsLib 形式化库。 地点：美国，AI 数学公司 Axiom Math。 人物：Ken Ono（Axiom Math 创始数学家）、Sidharth Hariharan（卡内基梅隆大学博士生，现为 Axiom Math 实习生，主导本次形式化工作）；被形式化成果的原作者包括牛津大学教授 James Maynard（2022 年菲尔兹奖得主）、陶哲轩（UCLA 教授）等 Polymath8b 协作组成员。 事件详情：Axiom Math 团队宣布，其自主多智能体 AI 系统 AxiomProver 首次自动完成了素数领域"246 定理"的形式化验证。该定理断言"存在无穷多对相差 246 的素数"，是目前人类在孪生素数猜想上取得的最强结果。形式化成果已开源在 GitHub 仓库 AxiomMath/PrimeGapsLib，采用 Lean 语言编写，包含三部分：PrimeGapsTheory（不含大规模数值计算的主证明）、PrimeGapsCert（耗时较长的大规模数值计算）以及合并库 PrimeGaps。仓库中同时给出了"由 Bombieri–Vinogradov 定理推出素数间隔无穷多次小于 600"和"结合数值证书推出间隔小于 246"两条主线结果，并提供 Comparator 形式化挑战文件，可用 leanprover/comparator 工具独立复核（完整校验耗时可达数小时）。Ken Ono 表示："该定理代表了人类目前对素数认知的边界。"Hariharan 指出，与一次性攻克单个难题的做法不同，Axiom Math 刻意把形式化组件设计成可复用模块，246 定理是这个素数间隔库中的旗舰结果。 背景：孪生素数猜想由法国数学家 Alphonse de Polignac 在 19 世纪首次精确表述，断言相差为 2 的素数对有无穷多组，至今未被证明。2013 年，现任中山大学教授的张益唐首次证明存在无穷多对间隔不超过 7000 万的素数，论文发表于《数学年刊》；几个月后 James Maynard 用另一套方法把上界从 7000 万压缩到 600，这项成果也是他获得 2022 年菲尔兹奖的重要依据；随后 Maynard 与陶哲轩等人组成的 Polymath8b 协作组进一步把上界降到 246。此前今年早些时候，Axiom Math 的竞争对手 Math, Inc. 曾用其 Gauss 智能体形式化了 Maryna Viazovska 关于 8 维与 24 维球堆积问题的菲尔兹奖级证明。需要注意的是，形式化验证并非 100% 保险，此前已有演示表明 Lean 内核漏洞可被利用，使系统接受一份由 AI 生成的错误证明。 影响：其一，这是 AI 系统首次自动验证当代数论前沿级别的证明，标志着 AI 辅助数学研究从"解题"走向"可复用的形式化基础设施"。其二，数论是当今密码学与网络安全的数学基础，被形式化的这批技术未来可用于验证加密方案的正确性。其三，Ken Ono 更看重的是外溢价值：他把证明形式化视为验证 AI 生成代码的跳板——如果算法是否终止、程序输出是否对任意输入都正确这类性质能被翻译成精确的数学命题，那么由 AxiomProver 衍生的技术就能对 AI 写出的代码做形式化证明。他警告说："世界即将运行在没人读过的代码之上。AI 已经来了，我们无法再回避——证明形式化是解决这一挑战的试验场。" 总结：Axiom Math 用 AxiomProver 首次自动形式化验证了"无穷多对素数相差 246"这一孪生素数猜想现有最强结果，代码以 Lean 开源。这既是 AI for Math 的里程碑，也被其团队视为通往"可验证 AI 生成代码"的关键一步。 参考来源： 1. IEEE Spectrum - Axiom Math Uses AI to Formally Verify 246 Theorem：https://spectrum.ieee.org/axiom-math-246-theorem-formalization 2. GitHub - AxiomMath/PrimeGapsLib（Lean 形式化开源库）：https://github.com/AxiomMath/PrimeGapsLib 3. Axiom Math 官网：https://axiommath.ai/ 4. GitHub - AxiomMath 组织仓库（axiom-lean-engine 等）：https://github.com/AxiomMath 5. arXiv - James Maynard《Small gaps between primes》：https://arxiv.org/abs/1311.4600 6. Annals of Mathematics - 张益唐《Bounded gaps between primes》：https://annals.math.princeton.edu/2014/179-3/p07 7. IEEE Spectrum - Watershed Moment for AI-Human Collaboration in Math：https://spectrum.ieee.org/ai-proof-verification 8. Math, Inc.（Gauss 智能体，形式化球堆积证明）：https://www.math.inc/ 9. Wolfram MathWorld - Twin Prime Conjecture：https://mathworld.wolfram.com/TwinPrimeConjecture.html