Apéry 式无理性证明：ζ(5) 与 Catalan 常数

问题

1979 年，Roger Apéry 用一对线性递推关系证明了 $\zeta(3)$ 是无理数。Epoch AI 的 FrontierMath Open Problems 将这个问题评为"突破级"，要求为其他著名常数给出同类证明。

AI 做了什么

Epoch AI 的"已解决"标签依据的是两项结果：

• $\zeta(5)$ 是无理数。 Aabir Fauzan（阿尔托大学）的预印本于 2026 年 9 月 17 日发布在 Zenodo 上。这个证明其实不是 Apéry 式的，但 Epoch AI 仍将问题记为已解决。Epoch 表示它认为这项工作符合"人与 AI 合作"的标准，但预印本页面和形式化仓库的说明里都没有提到 AI。
• Catalan 常数是无理数。 这是 OpenAI 于 2026 年 10 月 6 日集中发布的成果之一（第 005 组），预印本日期为 9 月 24 日。

如何验证

GitHub 用户 mo271 将 $\zeta(5)$ 的证明形式化为 Lean 代码。这个形式化是完整的，没有 sorry，只用了标准公理，并对照 Formal Conjectures 中该定理的陈述做了检查；它在一些常数和引理上与论文有所不同。Catalan 常数的结果只有 OpenAI 自己提供的 Lean 链接，没有独立核查。

局限

$\zeta(5)$ 的证明有很强的形式化证据支撑，但我们无法从一手资料确认 AI 在其中的贡献，因此在弄清之前将本条记为"待核实"。两篇预印本都未经同行评审。问题描述转述自 Epoch AI（CC BY 4.0）。

∎