微软研究院等证明 31 年未解的 KLS 猜想

微软研究院 Xinzhi Zhang 与合著者 Zhao Song 证明了 1995 年提出的 KLS 猜想，证明高维对数凹分布下平面切割与任意形状切割的差距可由与维度无关的常数界定。研究采用人类主导的智能体搜索流程，探索了 100 多条候选路径，由研究者筛选并递归应用新判据，最终在 2026 年 10 月 4 日版本中完成证明。同期另有独立团队给出完整证明，并有 Lean 4 形式化验证发布。