三项图谱特征值猜想得到 AI 辅助证明、反例与渐近加强，Lean 形式化分别进入 Palomar

Idris Ali Shaik 于 10 月 17 日发表图的最大两个邻接特征值研究：论文报告一个普遍谱不等式、对一项精确 color-critical 界的无限图族反例，以及含最大度修正项的 F-free 图渐近最优界。三项主定理均由 Lean 4 形式化，分别有 10 月 15、16、17 日 Palomar 登记。作者使用 ChatGPT 与 Codex 辅助探索、形式化及文稿检查，并声明自己审阅 AI 产物且承担责任；登记日期不应被误当成三个独立的新论文发布。