AI做数学的衡量标准，正在从“答对一道题”走向“把人类前沿证明完整翻译给机器检查”。Axiom Math公开了PrimeGapsLib：一套由AxiomProver参与生成、用Lean编写的素数间隔形式化库。它覆盖的旗舰结果不是新的数论定理，而是把数学界已知的“246界”变成可编译、可复核的证明代码。难点也正在这里——证明越长、依赖越多，形式化过程越接近真实研究，而不是短题演示。

先看结论：核验的是“至多246”，不是证明孪生素数

这个边界来自一条延续十余年的路线。2013年，张益唐把“存在无穷多对有界间隔素数”的上界推进到7000万；随后James Maynard将其降到600，Polymath8b协作又把公开结果压到246。孪生素数猜想要求间隔2同样无限出现，至今仍未解决。因此，“246定理”最准确的表述是素数间隔的已知上界，而不是存在无穷多对相差恰好246的素数。

Axiom公开库把主结果拆成多个层次：理论模块承载一般推导，证书模块处理大规模数值计算，组合模块给出完整结论。仓库还准备了只依赖Mathlib的挑战陈述，并使用Comparator核对实现与挑战是否一致。完整构建可能耗时数小时，较快版本则保留关键逻辑、减少重型计算，便于先做分钟级复核。

AxiomProver做的不是按下“检查”按钮

形式化证明首先要把论文中的自然语言、惯用省略和跨章节引用，改写成Lean能够解析的精确定义、引理与依赖关系。机器随后才能逐项确认类型、前提和推导是否成立。AxiomProver采用多智能体流程，把陈述翻译、子目标分解、证明搜索、代码修复和内核检查串起来；最终交付物不是一段解释性回答，而是一组可以重新编译的程序文件。

这也解释了246项目为何比竞赛题更有分量。短题通常边界清楚、依赖有限，而素数间隔证明涉及解析数论、筛法、既有库和大量计算证书。要让各部分在同一类型系统中闭合，系统既要找到局部证明，也要维持数千行代码之间的接口一致。公开库只有少量提交并不代表任务轻量，恰恰说明最终发布的是经过整理的证明产物，而非完整生成轨迹。

价值不只在数论：可复核输出开始追上生成能力

大模型擅长快速生成候选推导，但自然语言答案很难排除隐藏前提、符号误用和局部跳步。形式化系统把判断权交给小而确定的证明内核：只要代码能在指定环境中通过，至少说明它满足已经写入系统的形式规则。对数学研究而言，这能把审阅者从逐字符检查中释放出来，把注意力集中到定理陈述是否忠实、抽象是否有用，以及证明是否带来新的方法。

同一思路也能迁移到软件。程序终止性、输入输出约束和安全属性可以写成数学命题，再由证明器检查实现是否满足。AI生成代码越多，企业越需要一种独立于“模型自我解释”的验收机制。PrimeGapsLib展示的关键不是AI会写更多代码，而是生成结果可以被更小、更严格的系统拒绝或接受。

局限与编辑判断：形式化通过不等于所有问题自动消失

机器核验仍依赖一条信任链：原始定理有没有被准确翻译，使用的公理和库是否合适，数值证书是否覆盖应有范围，Lean内核、编译器与依赖版本是否可靠。若陈述本身写偏，系统可能严谨地证明“另一个命题”。目前仓库的审核标记仍以Axiom团队为主，外部数学家能否在独立环境完整复现，以及后续是否发现陈述或依赖问题，都需要持续观察。

ATYUN认为，这次进展的分水岭不在于246这个数字，而在于AI开始交付可公开复核的长证明工程。下一步值得追踪三件事：外部团队的复现结果、库中可复用引理被其他研究项目采用的情况，以及系统能否在更少人工整理下处理新的开放问题。只有当这三项同时推进，AI数学才会从漂亮演示变成稳定的研究基础设施。