Claude Fable 辅助将 Petrov 已知的整数多项式临界值定理构造成新证明并形式化于 Lean

RJ Acuna 于 10 月 21 日公开使用 Claude Fable 辅助的数论成果：给出 Petrov 关于任何代数数可实现为某个整数系数多项式临界值的独立构造证明，补充可实现多项式的分类和次数下界，并公布 Lean 4 形式化与在线计算器。作者称自己理解全部证明内容。**临界值覆盖代数闭包本身是早有 Petrov 论证的已知定理**，本事件记录新的独立证明、可复用形式化和构造性工具，而非 AI 首次发现该结论。10 月 21 日同日出现 v1 与 v2，以最新 v2 作为原始页面。