Axiom Math的AI在Lean中验证了246素数间隙定理

Axiom Math 表示其 AxiomProver 系统已经生成了一个机器检查的 Lean 4 证明，针对已知关于素数间隙: 即无限多对素数之间的差不超过 246 的定理。公司于 2026 年 8 月 17 日发布了该成果，作为一个交互式形式化蓝图，归功于 41 位命名的数学、工程和首席研究员贡献者，并由 IEEE Spectrum 首先报道 这一里程碑。

246 的界限是人类在长期攻克孪生素数猜想（19 世纪提出的假设，认为相差恰好为 2 的素数会无限出现）方面的最新进展。Axiom Math 的项目页面将这项工作描述为对 James Maynard 2013 年论文《Small gaps between primes》的统一形式化，以及 Polymath8b 合作后续中将 Maynard 的 600 界限收紧至 246 的部分。机器检查的证明被组织成一个公共的 Lean 库 PrimeGapsLib，246 定理是其旗舰成果。

“这一定理目前代表了人类对素数认知的极限，” Axiom Math 的创始数学家 Ken Ono 说。

形式化验证是指将证明翻译成一种小型、可信的程序（称为内核）能够逐行检查的语言。该结果并非绝对保证——命题本身必须被正确翻译，检查器也必须是可靠的——但它消除了人为裁判的易错性。迄今为止，参与数学基准测试的 AI 系统主要在带有简短、独立证明的竞赛题目上进行评估；这些结果与研究层面的形式化之间的差距很大，这一模式在 早期在奥林匹克几何中表现出色的系统 中可见，而研究数学基本未被触及。

从 7000 万到 246

该猜想本身由 19 世纪的 Alphonse de Polignac 精确表述，至今仍未被证明。首个有限界限出现在 2013 年，当时 Yitang Zhang 证明无限多对素数之间的距离不超过 7000 万。几个月后，Maynard 引入了一种改进的筛法，将界限削减至 600——这项工作帮助他获得了 2022 年的菲尔兹奖——随后包括 Maynard 和 Terence Tao 在内的 Polymath8b 合作将其进一步推至 246。Axiom Math 的蓝图将这一进程呈现为其计划形式化的项目。

形式化遵循公司描述的三阶段流程。研究人员首先将证明写成蓝图——为每个定义、引理和定理赋予标签、精确陈述以及其依赖的结果列表——生成了一个对工作进行排序的依赖图。随后，AxiomProver 这一公司用于通过形式化证明进行数学研究的多智能体系统，基于社区数学库 Mathlib 以及由 Alex Kontorovich 和 Tao 主导的已有形式化项目 PrimeNumberTheoremAnd，生成了可机器检查的 Lean 4 证明。Axiom 团队随后审查了生成的代码并将其组织进 PrimeGapsLib。

该库声明的主要成果略超标题定理。除了 246 界限外，还形式化了 Maynard 的 600 界限，并包含一个独立的验证挑战——仅基于 Mathlib，证明槽留空——允许任何拥有 Lean 比较工具的人独立确认库中的证明与所述定理相符。公司提醒，完整检查可能需要数小时；而覆盖另外两个结果的简化版本仅需数分钟即可完成。

此成果在 AI 形式化声明中的位置

该成果出现于 AI 系统进行研究级数学工作的声称不断升级的一年中，这些声称大多基于竞赛分数或简短证明。Axiom Math 是其中较为激进的声称者之一: AxiomProver 被认为解决了此前未解的问题，包括公司在同行评审期刊上发表的工作，并且 AI 系统已经解决了若干长期未解的 Erdős 问题。这次的 246 形式化属于不同类型的成果——不是新定理，而是对现代数论中技术要求最高的某个证明进行的机器检查重建。

最近的相似案例是今年早些时候，Math, Inc. 使用其 Gauss 代理完成了 Maryna Viazovska 在 8 维和 24 维空间的菲尔兹奖获奖球体堆砌结果的形式化证明。负责该形式化人类蓝图工作的卡内基梅隆大学博士生 Sidharth Hariharan 现为 Axiom Math 实习生，并在 246 项目中列为命名数学贡献者，他认为新成果更具综合性。他的理由是，Axiom 的构建面向重用: 与其一次性形式化单个证明，PrimeGapsLib 是一个维护中的素数间隙结果库，旨在支持未来的形式化工作和研究。

这种区别影响了对该成果的解读方式。一次性验证表明系统能够应对单个困难证明；而库则展示了更接近基础设施的特性——可重用的形式化工具，其他成果可以基于其构建——这正是 形式化证明系统正在发展的方向，它们正从解决练习转向检查真实数学。此处的能力主张基于公开且可重新运行的成果，而非基准分数: 蓝图、Lean 代码以及设计让外部研究者自行验证证明的比较挑战。

Ono 将数学视为更宏大目标的试验平台。他认为，如果软件的属性——例如程序是否终止、其输出是否对每个输入都正确——能够被表述为精确的数学命题，那么基于 AxiomProver 的系统就可以对其进行形式化证明，这指向对正在运行的基础设施、金融和安全系统中 AI 生成代码的验证。

“世界即将运行在没有人审阅的计算机代码上，” Ono 说。“AI 已经到来，我们再也无法视而不见——证明形式化是解决我认为我们将面对的 AI 最大挑战的试验平台。”

目前可交付的成果更为聚焦且可检验: 一个由 41 位作者完成的蓝图、一个公开的 Lean 库，以及一个机器验证的证明，表明相差不超过 246 的素数永不耗尽——这是孪生素数猜想最近的已验证邻居，也是迄今为止 AI 系统端到端检查的最深层研究数学成果。