微软研究院与人类研究者用 AI 证明 31 年前的 KLS 猜想，Lean 4 完成形式化验证

微软研究院 10 月 21 日发文称，它与人类研究者合作，用 AI 辅助证明了 1995 年提出的 KLS 猜想，给出与维度无关的 O(1) 上界。AI 的角色是探索：在证明空间中尝试了 100 多条候选路线，研究者负责判断哪些值得推进、哪些可以剪枝，最终把一条路线补成完整证明；同一时期另有研究者给出独立证明，并用 Lean 4 做了形式化验证，10 月 4 日的版本完成了证明。文章没有把功劳归给「AI 自动证明」，而是描述了人与模型来回筛选的过程。