AI 生成确定性因数分解 Lean 证明论文

Isaac Rudich 等作者发布论文，给出 Lean 证书，声称存在确定性图灵机可在 N^o(1) 步内算出每个 N 的最小质因数，对 n 位输入运行 Ck·2^(n/k) 步；此前确定性分解的最好上界是 N^(1/5+o(1))。 论文明确写明，思路和 Lean 证明由 AI（Anthropic 的 Claude Opus 5.5）生成。读者需检查的 Lean 陈述仅 13 行且只用 Mathlib，完整证明约 35,000 行。作者称他们没有阅读证明，证明由 Lean 检查。 因此，上述上界目前是 Lean 证书所支持的主张，而非作者人工审读确认的结果。

AI 根据报道生成 · 57 分钟前更新

还没有足够的连续观测数据，暂不绘制趋势。