数学家宣称 ζ(5) 无理性证明，Lean 形式化已公开在 GitHub

AlexKontorovich · x · 2026-09-24

数学家 Alex Kontorovich 发帖称 ζ(5) 被证明是无理数，并链接了一个 Lean 4 / Mathlib 形式化项目 mo271/Zeta5。

该仓库基于 A. Fauzan 2026 年 9 月 17 日的预印本《ζ(5) is irrational》，用 Lean v4.34.0-rc1 和固定版本的 Mathlib 形式化证明 ∃ x, Irrational x ∧ riemannZeta 5 = x。项目引用 PrimeNumberTheoremAnd 中的素数定理结果，CI 工作流使用 Comparator 校验 Solution.lean 确实证明了挑战命题，且证明仅依赖 propext、Classical.choice 和 Quot.sound 三条公理。Kontorovich 特别感叹「借助 AI 的帮助我们能学到什么」——这是 AI 辅助数学形式化的又一标志性案例，但证明本身的正确性仍待数学界同行评审。