独立复现 OpenAI 的 Lean 证明：ζ(s) 在 Re(s) > 7/8 无零点

研究者对 OpenAI 用 AI 模型生成的 Lean 证明做了独立复现，结论是证明通过检查。该证明声称 Riemann zeta 函数在 Re(s) > 7/8 时没有零点，比此前只排除 Re(s)=1 及左侧极窄区域的结果推进了一步，但不等于证明 Riemann 假设。证明规模约 2,900 个文件、近 50 万行，Lean 自带内核与另一套用 Rust 独立实现的 nanoda 内核都接受该证明，且只依赖 Lean 的三条标准公理。复现者指出若干未覆盖之处：两次检查由同一操作者在同一台机器上完成，尚无人从全新克隆独立复现；检查假设 OpenAI 仓库非对抗性，其构建配置与 23 个依赖补丁在 setup 阶段运行于 comparator 沙箱之外；OpenAI 的配置默认关闭第二内核（405 个中 402 个设为 false），本次复现将其打开。