Jacob Fox 与 Sanjana Das 借 AI 证明 Murty-Simon 猜想

斯坦福组合数学家 Jacob Fox 与 Sanjana Das 提交 arXiv 论文，证明直径-2 临界图边数至多 ⌊n²/4⌋ 的 Murty-Simon 猜想，等号仅在完全平衡二部图取得。⌊n²/4⌋ 上界的原始证明主要由 AI 找到，研究者随后简化证明并将相关思想扩展到全部 n。论文尚未经同行评审，但已使用 AI 生成的 Lean 形式化证明进行核对。