黎曼假设新证明获 AxiomProver 数小时内 Lean 形式化

黎曼假设研究近期取得重要进展：现已证明超过 67% 的黎曼 zeta 函数零点位于临界线上且为单零点。数论学家 Youness Lamzouri 在 arXiv 发布了一篇短小精悍的论文，为这一结果给出极为优雅的新证明，而 Axiom 团队的 AxiomProver 在数小时内即用 Lean 定理证明器完成了该证明的形式化验证，并已纳入论文附录。这是 AI 辅助形式化数学能力的又一次集中展示，值得关注。

已确认

• 新结果显示超过 67% 的 zeta 零点位于临界线上且为单零点，此前曾让 Anthropic 相关成果登上头条。
• Youness Lamzouri 在 arXiv 发布了该结果的新证明。
• AxiomProver 已将该证明完整形式化验证，写入论文附录；据 @lawrennd 转述，Ken Ono 透露团队用 Lean 完成了形式化。
• 据多条转发帖描述，形式化在数小时内完成。

为什么重要

• 将前沿数论成果快速形式化验证，可提升论文可信度并缩短同行验证周期。
• 该事件展示了 AI 定理证明工具（如 AxiomProver）在真实数学研究流程中的实用性，是 AI 辅助数学的标志性案例。

2026-09-03 ~ 2026-09-04 · 5 条相关

• 黎曼假设研究新进展:常数项空间项级证明获 Lean 形式化验证 — lawrennd · 2026-09-03
• 数学家给出黎曼猜想新证明，AxiomProver 数小时内完成 Lean 形式化 — soumitrashukla9 · 2026-09-03
• 黎曼猜想重大突破：67% 零点在临界线上，AI 已完成形式化验证 — burny_tech · 2026-09-04
• AxiomProver 已形式化验证黎曼猜想新证明,纳入论文附录 — burny_tech · 2026-09-04

另有 1 条近重复转述:Afinetheorem