论文：Axiom Math (Ken Ono 等 41 位贡献者). Formal Verification of the 246 Prime-Gaps Theorem via Lean 4 / PrimeGapsLib. IEEE Spectrum 首发报道, 2026-08-17. 蓝图: primegaps.axiommath.ai/paper/
补漏四条：
- "246 间隙"这条定理的上游是 Polymath8b 的接力赛,不是哪一个人的神来之笔。原帖讲"张益唐 2013 砍到 7000 万 → Maynard 600 → 联队 246",这条线其实跨了 13 年、6 轮主要改进。Axiom Math 的形式化蓝图诚实地把这条递进阶梯整条画出来(包含 Maynard 2014 筛法、Polymath8b 8b1/8b2/8b3 各次细化、最终收敛到 246),不是只挑一个最炫的数字塞进去。这种"全阶梯入库"对后续孪生素数猜想的形式化,等于白送了一幅路标图。
- 蓝图 → Lean 4 → 公开复核,三步走的设计哲学很值得单独说。原帖讲 Auto-formalizer + Conjecturer + 搜索引擎 + Auto-informalizer 四个模块,但更关键的是"人写蓝图、机器跑 Lean、人审产物"这种 Human-in-the-loop 结构。PrimeGapsLib 里专门留了一个"自包含验证挑战":把证明槽挖空,只留 Mathlib + 一个空 Lean 文件,谁拿 Linux 跑 lean comparator 都能复现那 41 个蓝图书章节是不是真的。这是 OpenAI Astra "Lean 4 证书"模式之外的第二条路——Astra 是"我证完你信我",Axiom 是"我证完你也能证"。
- Ken Ono 给的边界判据是"软件正确性证明的下一步"。原帖引用了"世界即将运行在没人读过的代码上"那句话但没展开。这意味着 Lean 4 形式化正在从"数学证明的玩具场"位移到"软件工程的基础设施"。一旦关键库(密码学、共识算法、操作系统内核)能用 PrimeGapsLib 范式做形式化,CSAF / NIST 这类标准组织的合规清单就要重写。Axiom Math 把这件事从数学家手里抢过来,第一次让"AI 写代码 + AI 验代码"成了商业可投资的事。
- 这条管线的真实瓶颈不是"AI 写 Lean 4 的能力",而是"人类对原始证明的形式化翻译"。原帖把"显然""容易验证"这些跳步拆成子目标说得很轻,但实际上一份研究级证明被拆成几千个 Lean 引理,每一个都需要数学家判断"这个跳步能不能被合法化"。41 位贡献者、3 个月的蓝图编写,大量时间花在"决定这条引理的边界在哪"上。AI 加速了"机器跑 Lean",但"决定该跑什么"还是数学家的事——这是这条范式的真实边界。