Claude Opus 5.5 单次会话生成 Roy 强六指数定理及 Waldschmidt/Philippon 辅助理论的 Lean 4 形式化

Shawn Krisman 于 10 月 18 日发布 Lean 4 / Mathlib 形式化成果，声称完整覆盖 Roy 的强六指数定理：对于两组分别在代数数域上线性无关的 2 个与 3 个复数，六个乘积中至少一个不属于由 1 和代数数对数张成的向量空间。证明链还形式化 Waldschmidt 的超越性定理及 Philippon 的重数估计，仓库公开 Lean 源码，报告仅使用 Lean 标准三条公理闭合。作者披露代码通过一次 Claude Code 会话、使用 Claude Opus 5.5 生成，Hexagon 标记 human understanding 为 no parts。本条是已有经典数学定理的新形式化，不是新发现该超越性定理；编译声明来自提交者，尚未由 Radar 独立复跑。