Lean 4 完整形式化 ζ(5) 无理性证明，仓库已开源
AlexKontorovich · x · 2026-09-24
数学家 Moritz Firsching 宣布完成 ζ(5) 无理性证明的 Lean 4 形式化，仓库 Zeta5 已开源。
关键信息：
- 项目基于 A. Fauzan 的预印本《ζ(5) is irrational》，目标是形式化命题 riemannZeta 5 = x ∧ Irrational x
- 核心是 Apery 式有理逼近构造，素数定理（θ id）依赖 PrimeNumberTheoremAnd 库
- 证明由 Solution.lean 从 Apery.irrationalfive 推出 Formal Conjectures 中的基准声明
- CI 用 Comparator 自动校验：证明确实成立、且只依赖 propext、Classical.choice、Quot.sound 三条公理
- 工具链为 Lean v4.34.0-rc1，Mathlib 锁定在特定 commit，Apache 2.0 协议
ζ(5) 的无理性此前只是新预印本的主张，如今已被证明助手完全机器检验，是形式化数学圈内的重要事件。
所属事件:ζ(5) 无理性获证明，数小时内完成 Lean 形式化(4 条相关)→
「研究」频道最新
- AI 管线扫描 Linux 内核发现 2386 个漏洞,170 个补丁已合入主线 — ycombinator · 2026-11-12
- CoRL 联合主席忆 2021 展区仅三张桌，对比 2026 规模感概行业巨变 — Ed__Johns · 2026-11-12
- 预训练原子模型筛选 1620 种组合，为单原子金属找稳定衬底 — bravo_abad · 2026-11-12
- Claude Fable 5.2 机器人实验被拿去吊打李飞飞 World Labs?作者称搞错了研究问题 — dotey · 2026-11-12
- Claude 数周产出 239 个形式化证明,验证 123 个开源库无崩溃 — kieranklaassen · 2026-11-12
- SynthICL：纯合成数据训练，单演示泛化 16 项真实操作任务 — Ed__Johns · 2026-11-12