Claude 协助提升 Lehmer 欧拉函数问题因子个数下界至 16，并以 Lean 与双实现有限计算作证

Deep Bhattacharjee 于 10 月 22 日公布关于 Lehmer's totient problem 的新排除范围：若复合数 n 满足 φ(n)∣n−1，则其不同素因子至少有 16 个；论文进一步对 (n−1)/φ(n)≥3、3∣n 等情形给出更强限制，并检查 φ(n)∣n+1 的小因子例外。Claude Code 负责搜索、证明程序、部分不依赖搜索的 Lean 证明及初稿，作者审核修改。关键有限检查由独立编写的 Python 与 PARI/GP 程序执行且有日志。**Lehmer 猜想本身仍未解决**；形式化仅覆盖指定推导，计算证书不等同全部无条件 Lean 证明。