Claude 5.5 生成并 Lean 全核验新无理性结果：β(4), β(6), …, β(36) 至少一个无理

Shawn Krisman 于 10 月 16 日公开一项 primarily AI-generated 数论结果及完整 Lean 4 certificate：Dirichlet beta function 的 17 个偶数值 β(4),β(6),…,β(36) 中至少一个是无理数。与已有显式结果常包含 Catalan 常数 β(2) 不同，新结论完全排除 β(2)。证明沿 Ball–Rivoal / Rivoal–Zudilin 路线构造二阶导数线性形式，通过 p-adic denominator analysis、精确有理证书、实轴 size bound 与 saddle-point nonvanishing 完成；仓库包含 62,131 个 event intervals 等数值证书，全部在 Lean kernel 中检查。项目由两次 Claude Opus 5.5 sessions 主导产生，仓库于 10 月 16 日创建；作者明确说明尚无人类专家审阅数学或 Lean 代码。