事件观察中
第三方独立复核 OpenAI 的 Lean 数学证明
先了解这件事
AI 综述
有研究者对 OpenAI 用 AI 模型生成的 Lean 证明做了独立复现，结论是证明通过检查。该证明声称 Riemann zeta 函数在 Re(s) > 7/8 时没有零点，比此前只排除 Re(s)=1 及左侧极窄区域的结果推进了一步，但不等于证明 Riemann 假设。证明规模约 2,900 个文件、近 50 万行，Lean 自带内核与另一套用 Rust 独立实现的 nanoda 内核都接受该证明，且只依赖 Lean 的三条标准公理。
AI 根据报道生成 · 18 小时前更新
最新进展10月8日 20:26
研究者独立复现 OpenAI 的 Lean 证明，结论是证明通过检查。后续时间线
10月8日
- davegoldblatt/openai-zeta-proof-check精选独立复现 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），本次复现将其打开。
相关讨论
关注度走势
每天新增来源
- 10月8日 新增 1 个来源（1 家媒体、0 个账号）
- 10月9日 新增 0 个来源（0 家媒体、0 个账号）
- 10月10日 新增 0 个来源（0 家媒体、0 个账号）