Fable 与 Claude 协作形式化 (3/2)^n steering word 超线性复杂度定理，10 月 20 日获得 Palomar 新登记

Ralf Stephan 于 10 月 20 日发布新版本相关研究的 Hexagon 页面及 Palomar 形式化登记 PALOMAR-2026-10-20-000014，报告把 (3/2)^n 最近整数编码得到的 steering word T 的子词复杂度 p_T(k)/k→∞ 连同使用的 p-adic Subspace Theorem 全部形式化于 Lean 4。作者披露 Fable 5 探索新证明，Opus 4.8/5 协助 Lean 开发，数论专家 Yann Bugeaud 提供评论并建议简化，Fable 5.1 生成后续简化论证。该题材已有 arXiv:2607.11648 早期版本；10 月 20 日仅记录新增 Palomar/Lean 核验公开里程碑，不主张定理首次在当天提出，且未在本轮独立核验 kernel 运行。