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

微软研究院研究员 Xinzhi Zhang 与合著者 Zhao Song 证明了 1995 年提出的 KLS 猜想，给出与维度无关的固定界，解决了高维几何与概率论的核心开放问题。证明过程采用人类引导的智能体搜索，探索了 100 多条候选路径，由研究者筛选和调整方向；同期另有独立团队给出完整证明，并出现 Lean 4 形式化验证。作者称此前用多个前沿模型做无引导的端到端尝试未能成功。