微软研究者用人类主导的智能体流程证明 31 年未解的 KLS 猜想

微软研究院研究者 Xinzhi Zhang 与合作者证明了 1995 年提出的 KLS 猜想，确认高维下最优平面切与任意形状最优切之间的差距由固定常数界定，不随维度增长。完整证明在 2026 年 10 月 4 日版本中完成，此前 7 月的最好结果只允许该界随维度缓慢增长。研究通过人类主导的智能体搜索探索了约 100 条路径，同期另有独立团队给出完整证明，并已有 Lean 4 形式化验证。