Claude 多 Agent 提出 Catalan 常数相关表达式与 L 值的无理性指数新上界，报告 Lean 完整形式验证

Sean Litsey 于 10 月 20 日公开主要由 Claude Opus、Sonnet、Haiku 5.5 Agent 在 Claude Code 中生成的数论结果，报告 μ(G±5π²/48)≤38.35、μ(L(2,χ₋₃))≤23.82；对于后者，相比作者所引以前的有效界 μ≤24781 大幅改进。其方法由 OpenAI 的 Catalan 常数行列式工作衍生，结合 p-adic 分母估计、Jacobi 矩阵与离散能量界；论文声明所有主结果均以 Lean 4 形式化，没有未证明步骤且仅依赖标准公理。公开声明 human understanding no parts，尚缺 Radar 的实际 Lean 重放与第三方专家核查。