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 条相关)→
「研究」频道最新
- Courant 研究者探讨 AI 生成 Lean 验证证明的人类可读性问题 — Pascallisch · 2026-09-24
- 质疑「LLM 痛觉轴」:静态词向量也能复现同样结论 — wschroll · 2026-09-24
- 对比学习语言模型 CLM-8B:推理快至 9 倍,刷榜智能体编码基准 — ChengleiSi · 2026-09-24
- 腾讯 ARC 发布 GAE：几何原生潜空间，FVD 最高降 23% — CSProfKGD · 2026-09-24
- OpenRSI 团队阐述 RSI 理念:智能体扩展洞见生成是 ASI 关键拼图 — ChengleiSi · 2026-09-24
- OpenRSI-Index 扩张招募领域负责人与算力合作伙伴 — ChengleiSi · 2026-09-24